--- a/src/Pure/goal.ML Fri Oct 21 18:17:00 2005 +0200
+++ b/src/Pure/goal.ML Fri Oct 21 18:20:29 2005 +0200
@@ -36,8 +36,8 @@
(* managing goal states *)
(*
- ----------------- (init)
- Goal C ==> Goal C
+ ------------ (init)
+ C ==> Goal C
*)
fun init ct = Drule.instantiate' [] [SOME ct] Drule.goalI;
@@ -56,7 +56,7 @@
Goal C
------ (finish)
C
-*)
+*)
fun finish th =
(case Thm.nprems_of th of
0 => conclude th
@@ -67,7 +67,7 @@
(* prove_raw -- minimal checks, no normalization *)
-fun prove_raw thy goal tac =
+fun prove_raw thy goal tac =
(case SINGLE tac (init (Thm.cterm_of thy goal)) of
SOME th => finish th
| NONE => raise ERROR_MESSAGE "Tactic failed.");
@@ -157,7 +157,6 @@
else Seq.empty
end;
-
end;
structure BasicGoal: BASIC_GOAL = Goal;