--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Aug 25 18:26:58 2010 +0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Aug 25 20:04:49 2010 +0800
@@ -310,7 +310,7 @@
-(* Injection means to prove that the regularised theorem implies
+(* Injection means to prove that the regularized theorem implies
the abs/rep injected one.
The deterministic part:
@@ -541,8 +541,7 @@
end
-
-(** Tactic for Generalising Free Variables in a Goal **)
+(* Tactic for Generalising Free Variables in a Goal *)
fun inst_spec ctrm =
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
@@ -649,6 +648,7 @@
(** lifting as a tactic **)
+
(* the tactic leaves three subgoals to be proved *)
fun lift_procedure_tac ctxt rthm =
Object_Logic.full_atomize_tac
@@ -691,7 +691,7 @@
val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
in
Goal.prove ctxt' [] [] goal
- (K (HEADGOAL (asm_full_simp_tac ss THEN' lift_single_tac ctxt' rthm'')))
+ (K (EVERY1 [asm_full_simp_tac ss, lift_single_tac ctxt' rthm'']))
|> singleton (ProofContext.export ctxt' ctxt)
end