src/HOL/Tools/inductive_realizer.ML
changeset 36610 bafd82950e24
parent 36043 d149c3886e7e
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -137,7 +137,7 @@
     1.4  
     1.5  fun fun_of_prem thy rsets vs params rule ivs intr =
     1.6    let
     1.7 -    val ctxt = ProofContext.init thy
     1.8 +    val ctxt = ProofContext.init_global thy
     1.9      val args = map (Free o apfst fst o dest_Var) ivs;
    1.10      val args' = map (Free o apfst fst)
    1.11        (subtract (op =) params (Term.add_vars (prop_of intr) []));
    1.12 @@ -484,7 +484,7 @@
    1.13  fun add_ind_realizers name rsets thy =
    1.14    let
    1.15      val (_, {intrs, induct, raw_induct, elims, ...}) =
    1.16 -      Inductive.the_inductive (ProofContext.init thy) name;
    1.17 +      Inductive.the_inductive (ProofContext.init_global thy) name;
    1.18      val vss = sort (int_ord o pairself length)
    1.19        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
    1.20    in