--- a/src/HOL/Tools/enriched_type.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/enriched_type.ML Wed Mar 27 14:19:18 2013 +0100
@@ -125,7 +125,7 @@
(mapper21 $ (mapper32 $ x), mapper31 $ x);
val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
- fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop
+ fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
(K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
THEN' Simplifier.asm_lr_simp_tac compositionality_ss
THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
@@ -148,7 +148,7 @@
val rhs = HOLogic.id_const T;
val (id_prop, identity_prop) = pairself
(HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
- fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop
+ fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
(K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss)));
in (id_prop, prove_identity) end;