--- a/src/HOL/Tools/inductive_realizer.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Mon May 03 14:25:56 2010 +0200
@@ -137,7 +137,7 @@
fun fun_of_prem thy rsets vs params rule ivs intr =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val args = map (Free o apfst fst o dest_Var) ivs;
val args' = map (Free o apfst fst)
(subtract (op =) params (Term.add_vars (prop_of intr) []));
@@ -484,7 +484,7 @@
fun add_ind_realizers name rsets thy =
let
val (_, {intrs, induct, raw_induct, elims, ...}) =
- Inductive.the_inductive (ProofContext.init thy) name;
+ Inductive.the_inductive (ProofContext.init_global thy) name;
val vss = sort (int_ord o pairself length)
(subsets (map fst (relevant_vars (concl_of (hd intrs)))))
in