src/HOL/Nominal/nominal_inductive.ML
changeset 33968 f94fb13ecbb3
parent 33772 b6a1feca2ac2
child 35232 f588e1169c8b
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Nov 30 11:42:48 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Nov 30 11:42:49 2009 +0100
     1.3 @@ -247,7 +247,7 @@
     1.4        end) prems);
     1.5  
     1.6      val ind_vars =
     1.7 -      (DatatypeProp.indexify_names (replicate (length atomTs) "pi") ~~
     1.8 +      (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 @@ -647,7 +647,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 -        (DatatypeAux.split_conj_thm (Goal.prove ctxt' [] []
    1.17 +        (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;