@@ -1187,8 +1187,8 @@ reifyApp _ t [x]
1187reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
1187reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
1188reifyApp ist t [Constant (Str n), x]
1188reifyApp ist t [Constant (Str n), x]
1189 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
1189 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
1190−reifyApp _ t [Constant (Str n)]
1190+reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
1191− | t == reflm "Intro" = return $ Intro [sUN n]
1191+reifyApp _ t [n] | t == reflm "Induction" = liftM Induction (reifyTTName n)
1192reifyApp ist t [t']
1192reifyApp ist t [t']
1193 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
1193 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
1194reifyApp ist t [t']
1194reifyApp ist t [t']