src/ZF/Tools/datatype_package.ML
changeset 35989 3418cdf1855e
parent 35409 5c5bb83f2bae
child 36610 bafd82950e24
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Mar 27 17:36:32 2010 +0100
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 27 18:07:21 2010 +0100
     1.3 @@ -108,7 +108,7 @@
     1.4      let val ncon = length con_ty_list    (*number of constructors*)
     1.5          fun mk_def (((id,T,syn), name, args, prems), kcon) =
     1.6                (*kcon is index of constructor*)
     1.7 -            Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
     1.8 +            OldGoals.mk_defpair (list_comb (Const (full_name name, T), args),
     1.9                          mk_inject npart kpart
    1.10                          (mk_inject ncon kcon (mk_tuple args)))
    1.11      in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
    1.12 @@ -157,7 +157,7 @@
    1.13    val case_const = Const (case_name, case_typ);
    1.14    val case_tm = list_comb (case_const, case_args);
    1.15  
    1.16 -  val case_def = Primitive_Defs.mk_defpair
    1.17 +  val case_def = OldGoals.mk_defpair
    1.18      (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
    1.19  
    1.20  
    1.21 @@ -232,7 +232,7 @@
    1.22    val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
    1.23  
    1.24    val recursor_def =
    1.25 -      Primitive_Defs.mk_defpair
    1.26 +      OldGoals.mk_defpair
    1.27          (recursor_tm,
    1.28           @{const Univ.Vrecursor} $
    1.29             absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));