src/HOL/Nominal/nominal_inductive.ML
changeset 58112 8081087096ad
parent 57884 36b5691b81a5
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 01 16:17:46 2014 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 01 16:17:46 2014 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4        end) prems);
     1.5  
     1.6      val ind_vars =
     1.7 -      (Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
     1.8 +      (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
     1.9         map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
    1.10      val ind_Ts = rev (map snd ind_vars);
    1.11  
    1.12 @@ -645,7 +645,7 @@
    1.13      val thss = map (fn atom =>
    1.14        let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])))
    1.15        in map (fn th => zero_var_indexes (th RS mp))
    1.16 -        (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
    1.17 +        (Old_Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
    1.18            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
    1.19              let
    1.20                val (h, ts) = strip_comb p;