src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Sat Jan 20 14:09:23 2007 +0100
+++ b/src/FOL/FOL.thy	Sat Jan 20 14:09:27 2007 +0100
@@ -55,13 +55,8 @@
 
 (*For disjunctive case analysis*)
 ML {*
-  local
-    val excluded_middle = thm "excluded_middle"
-    val disjE = thm "disjE"
-  in
-    fun excluded_middle_tac sP =
-      res_inst_tac [("Q",sP)] (excluded_middle RS disjE)
-  end
+  fun excluded_middle_tac sP =
+    res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE})
 *}
 
 lemma case_split_thm:
@@ -77,11 +72,7 @@
 
 (*HOL's more natural case analysis tactic*)
 ML {*
-  local
-    val case_split_thm = thm "case_split_thm"
-  in
-    fun case_tac a = res_inst_tac [("P",a)] case_split_thm
-  end
+  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split_thm}
 *}
 
 
@@ -278,10 +269,10 @@
 ML {*
   structure InductMethod = InductMethodFun
   (struct
-    val cases_default = thm "case_split";
-    val atomize = thms "induct_atomize";
-    val rulify = thms "induct_rulify";
-    val rulify_fallback = thms "induct_rulify_fallback";
+    val cases_default = @{thm case_split}
+    val atomize = @{thms induct_atomize}
+    val rulify = @{thms induct_rulify}
+    val rulify_fallback = @{thms induct_rulify_fallback}
   end);
 *}