# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID 973d18ad2a738f3400eecb6ff9d57ac01fd9c4d0
# Parent  1413c62db67500492ec4397d982e41a4c702b9d0
importing theorems correctly causes problems with mutual recursive predicates in the predicate compiler; must be discussed with Stefan first

diff -r 1413c62db675 -r 973d18ad2a73 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -291,7 +291,7 @@
 
 fun mk_casesrule ctxt nparams introrules =
   let
-    val (intros_th, ctxt1) = import_intros introrules ctxt
+    val ((_, intros_th), ctxt1) = Variable.import false introrules ctxt
     val intros = map prop_of intros_th
     val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
     val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
@@ -2174,7 +2174,7 @@
     
 fun prepare_intrs thy prednames intros =
   let
-    val (intrs, _) =  import_intros intros (ProofContext.init thy)
+    val ((_, intrs), _) = Variable.import false intros (ProofContext.init thy)
     val intrs = map prop_of intrs
     val nparams = nparams_of thy (hd prednames)
     val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)