src/HOL/Tools/inductive_realizer.ML
changeset 28965 1de908189869
parent 28814 463c9e9111ae
child 29265 5b4247055bd7
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -338,7 +338,7 @@
     1.4              (Logic.strip_assums_concl rintr));
     1.5            val s' = Sign.base_name s;
     1.6            val T' = Logic.unvarifyT T
     1.7 -        in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
     1.8 +        in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
     1.9      val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
    1.10        (List.take (snd (strip_comb
    1.11          (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
    1.12 @@ -347,10 +347,10 @@
    1.13  
    1.14      val (ind_info, thy3') = thy2 |>
    1.15        InductivePackage.add_inductive_global (serial_string ())
    1.16 -        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding,
    1.17 +        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
    1.18            coind = false, no_elim = false, no_ind = false, skip_mono = false}
    1.19          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.20 -          ((Name.binding (Sign.base_name (name_of_thm intr)), []),
    1.21 +          ((Binding.name (Sign.base_name (name_of_thm intr)), []),
    1.22             subst_atomic rlzpreds' (Logic.unvarify rintr)))
    1.23               (rintrs ~~ maps snd rss)) [] ||>
    1.24        Sign.absolute_path;