src/HOL/Tools/inductive_realizer.ML
changeset 42361 23f352990944
parent 39557 fe5722fce758
child 42375 774df7c59508
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -136,7 +136,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_global thy
     1.8 +    val ctxt = Proof_Context.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 @@ -483,7 +483,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_global thy) name;
    1.17 +      Inductive.the_inductive (Proof_Context.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