src/HOL/Tools/inductive_realizer.ML
changeset 30345 76fd85bbf139
parent 30280 eb98b49ef835
child 30364 577edc39b501
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 07 22:16:50 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 07 22:17:25 2009 +0100
     1.3 @@ -68,8 +68,8 @@
     1.4      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
     1.5        (Logic.strip_imp_concl (prop_of (hd intrs))));
     1.6      val params = map dest_Var (Library.take (nparms, ts));
     1.7 -    val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs);
     1.8 -    fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr),
     1.9 +    val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs));
    1.10 +    fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)),
    1.11        map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
    1.12          filter_out (equal Extraction.nullT) (map
    1.13            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    1.14 @@ -234,7 +234,7 @@
    1.15    end;
    1.16  
    1.17  fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
    1.18 -  if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
    1.19 +  if Binding.eq_name (name, s) then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
    1.20    else x;
    1.21  
    1.22  fun add_dummies f [] _ thy =
    1.23 @@ -242,14 +242,14 @@
    1.24    | add_dummies f dts used thy =
    1.25        thy
    1.26        |> f (map snd dts)
    1.27 -      |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
    1.28 +      |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
    1.29      handle DatatypeAux.Datatype_Empty name' =>
    1.30        let
    1.31          val name = NameSpace.base_name name';
    1.32 -        val dname = Name.variant used "Dummy"
    1.33 +        val dname = Name.variant used "Dummy";
    1.34        in
    1.35          thy
    1.36 -        |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
    1.37 +        |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
    1.38        end;
    1.39  
    1.40  fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
    1.41 @@ -296,7 +296,7 @@
    1.42  
    1.43      val thy1' = thy1 |>
    1.44        Theory.copy |>
    1.45 -      Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |>
    1.46 +      Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |>
    1.47        fold (fn s => AxClass.axiomatize_arity
    1.48          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
    1.49          Extraction.add_typeof_eqns_i ty_eqs;
    1.50 @@ -308,7 +308,7 @@
    1.51      val ((dummies, dt_info), thy2) =
    1.52        thy1
    1.53        |> add_dummies
    1.54 -           (DatatypePackage.add_datatype false false (map #2 dts))
    1.55 +           (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
    1.56             (map (pair false) dts) []
    1.57        ||> Extraction.add_typeof_eqns_i ty_eqs
    1.58        ||> Extraction.add_realizes_eqns_i rlz_eqs;
    1.59 @@ -330,14 +330,17 @@
    1.60          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
    1.61            (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
    1.62              (maps snd rss ~~ List.concat constrss);
    1.63 -    val (rlzpreds, rlzpreds') = split_list
    1.64 -      (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
    1.65 +    val (rlzpreds, rlzpreds') =
    1.66 +      rintrs |> map (fn rintr =>
    1.67          let
    1.68 -          val Const (s, T) = head_of (HOLogic.dest_Trueprop
    1.69 -            (Logic.strip_assums_concl rintr));
    1.70 +          val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
    1.71            val s' = NameSpace.base_name s;
    1.72 -          val T' = Logic.unvarifyT T
    1.73 -        in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
    1.74 +          val T' = Logic.unvarifyT T;
    1.75 +        in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
    1.76 +      |> distinct (op = o pairself (#1 o #1))
    1.77 +      |> map (apfst (apfst (apfst Binding.name)))
    1.78 +      |> split_list;
    1.79 +
    1.80      val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
    1.81        (List.take (snd (strip_comb
    1.82          (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));