--- a/src/HOL/Tools/record_package.ML Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Tools/record_package.ML Thu Mar 20 12:09:20 2008 +0100
@@ -64,8 +64,8 @@
val meta_allE = thm "Pure.meta_allE";
val prop_subst = thm "prop_subst";
val Pair_sel_convs = [fst_conv,snd_conv];
-val K_record_comp = thm "K_record_comp";
-val K_comp_convs = [o_apply, K_record_comp]
+val K_record_comp = @{thm "K_record_comp"};
+val K_comp_convs = [@{thm o_apply}, K_record_comp]
(** name components **)
@@ -2063,7 +2063,7 @@
in
prove_standard [assm] concl (fn {prems, ...} =>
try_param_tac rN induct_scheme 1
- THEN try_param_tac "more" unit_induct 1
+ THEN try_param_tac "more" @{thm unit_induct} 1
THEN resolve_tac prems 1)
end;
val induct = timeit_msg "record induct proof:" induct_prf;