--- a/src/HOL/Tools/inductive.ML Fri Sep 18 09:07:48 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Sep 18 09:07:49 2009 +0200
@@ -86,13 +86,13 @@
(** theory context references **)
val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
+val inductive_forall_def = @{thm induct_forall_def};
val inductive_conj_name = "HOL.induct_conj";
-val inductive_conj_def = thm "induct_conj_def";
-val inductive_conj = thms "induct_conj";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
-val inductive_rulify_fallback = thms "induct_rulify_fallback";
+val inductive_conj_def = @{thm induct_conj_def};
+val inductive_conj = @{thms induct_conj};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
+val inductive_rulify_fallback = @{thms induct_rulify_fallback};
val notTrueE = TrueI RSN (2, notE);
val notFalseI = Seq.hd (atac 1 notI);
@@ -176,7 +176,7 @@
case concl of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
| _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
- | _ $ (Const ("HOL.ord_class.less_eq", _) $ _ $ _) =>
+ | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
[dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [le_funI, le_boolI'])) thm))]
| _ => [thm]