src/LCF/LCF.thy
 changeset 27208 5fe899199f85 parent 22810 a8455ca995d6 child 27239 f2f42f9fa09d
```--- a/src/LCF/LCF.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/LCF.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -23,7 +23,7 @@
typedecl ('a,'b) "+"    (infixl 5)

arities
-  fun :: (cpo, cpo) cpo
+  "fun" :: (cpo, cpo) cpo
"*" :: (cpo, cpo) cpo
"+" :: (cpo, cpo) cpo
tr :: cpo
@@ -316,13 +316,13 @@

ML {*
-  fun induct_tac v i =
-    res_inst_tac[("f",v)] @{thm induct} i THEN
+  fun induct_tac ctxt v i =
+    RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
REPEAT (resolve_tac @{thms adm_lemmas} i)
*}

lemma least_FIX: "f(p) = p ==> FIX(f) << p"
-  apply (tactic {* induct_tac "f" 1 *})
+  apply (tactic {* induct_tac @{context} "f" 1 *})
apply (rule minimal)
apply (intro strip)
apply (erule subst)
@@ -375,8 +375,8 @@
done

ML {*
-fun induct2_tac (f,g) i =
-  res_inst_tac[("f",f),("g",g)] @{thm induct2} i THEN
+fun induct2_tac ctxt (f, g) i =
+  RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
REPEAT(resolve_tac @{thms adm_lemmas} i)
*}
```