# HG changeset patch
# User wenzelm
# Date 1177590253 -7200
# Node ID a8455ca995d6e348fed8944c19f4c1287d14cf8c
# Parent  3cf5df73d50a1c9c9403bafc34d481cdd97f2f00
eliminated unnamed infixes;
tuned ML setup;

diff -r 3cf5df73d50a -r a8455ca995d6 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Thu Apr 26 14:24:12 2007 +0200
+++ b/src/LCF/LCF.thy	Thu Apr 26 14:24:13 2007 +0200
@@ -43,7 +43,7 @@
  VOID   :: "void"               ("'(')")
  PAIR   :: "['a,'b] => 'a*'b"   ("(1<_,/_>)" [0,0] 100)
  COND   :: "[tr,'a,'a] => 'a"   ("(_ =>/ (_ |/ _))" [60,60,60] 60)
- "<<"   :: "['a,'a] => o"       (infixl 50)
+ less   :: "['a,'a] => o"       (infixl "<<" 50)
 
 axioms
   (** DOMAIN THEORY **)
@@ -316,13 +316,9 @@
 
 
 ML {*
-local
-  val adm_lemmas = thms "adm_lemmas"
-  val induct = thm "induct"
-in
   fun induct_tac v i =
-    res_inst_tac[("f",v)] induct i THEN REPEAT (resolve_tac adm_lemmas i)
-end
+    res_inst_tac[("f",v)] @{thm induct} i THEN
+    REPEAT (resolve_tac @{thms adm_lemmas} i)
 *}
 
 lemma least_FIX: "f(p) = p ==> FIX(f) << p"
@@ -379,16 +375,9 @@
   done
 
 ML {*
-local
-  val induct2 = thm "induct2"
-  val adm_lemmas = thms "adm_lemmas"
-in
-
 fun induct2_tac (f,g) i =
-  res_inst_tac[("f",f),("g",g)] induct2 i THEN
-  REPEAT(resolve_tac adm_lemmas i)
-
-end
+  res_inst_tac[("f",f),("g",g)] @{thm induct2} i THEN
+  REPEAT(resolve_tac @{thms adm_lemmas} i)
 *}
 
 end