# HG changeset patch
# User wenzelm
# Date 1204199793 -3600
# Node ID 6b127c056e833c9eb0e09355720a025d6553b03e
# Parent  038baad81209c2183e8adeaf84bca65fb219c0dd
removed legacy ML bindings;

diff -r 038baad81209 -r 6b127c056e83 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Thu Feb 28 12:56:31 2008 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Thu Feb 28 12:56:33 2008 +0100
@@ -451,7 +451,7 @@
          (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) theory addsimps case_rewrites)
      val corollaries' = map (Simplifier.simplify case_ss) corollaries
      val extract = R.CONTEXT_REWRITE_RULE
-                     (f, [R], cut_apply, meta_tflCongs@context_congs)
+                     (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs)
      val (rules, TCs) = ListPair.unzip (map extract corollaries')
      val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
      val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
@@ -508,7 +508,7 @@
      val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
      val corollaries' = map (rewrite_rule case_rewrites) corollaries
      fun extract X = R.CONTEXT_REWRITE_RULE
-                       (f, R1::SV, cut_apply, tflCongs@context_congs) X
+                       (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
  in {proto_def = proto_def,
      SV=SV,
      WFR=WFR,