typedef etc.: no constraints;
authorwenzelm
Fri Mar 19 00:47:23 2010 +0100 (2010-03-19)
changeset 358427c170d39a808
parent 35841 94f901e4969a
child 35843 23908b4dbc2f
typedef etc.: no constraints;
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Quotient/quotient_typ.ML
src/HOL/Tools/typecopy.ML
src/HOLCF/Tools/Domain/domain_isomorphism.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Mar 19 00:46:08 2010 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Mar 19 00:47:23 2010 +0100
     1.3 @@ -2095,7 +2095,7 @@
     1.4              val typ = (tycname,tnames,tsyn)
     1.5              val ((_, typedef_info), thy') =
     1.6                Typedef.add_typedef_global false (SOME (Binding.name thmname))
     1.7 -                (Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy
     1.8 +                (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy
     1.9              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
    1.10  
    1.11              val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
    1.12 @@ -2182,7 +2182,8 @@
    1.13              val tsyn = mk_syn thy tycname
    1.14              val typ = (tycname,tnames,tsyn)
    1.15              val ((_, typedef_info), thy') =
    1.16 -              Typedef.add_typedef_global false NONE (Binding.name tycname,tnames,tsyn) c
    1.17 +              Typedef.add_typedef_global false NONE
    1.18 +                (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c
    1.19                  (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
    1.20              val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
    1.21              val fulltyname = Sign.intern_type thy' tycname
     2.1 --- a/src/HOL/Import/replay.ML	Fri Mar 19 00:46:08 2010 +0100
     2.2 +++ b/src/HOL/Import/replay.ML	Fri Mar 19 00:47:23 2010 +0100
     2.3 @@ -343,7 +343,8 @@
     2.4            | delta (Hol_theorem (thyname, thmname, th)) thy =
     2.5              add_hol4_theorem thyname thmname ([], th_of thy th) thy
     2.6            | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
     2.7 -            snd (Typedef.add_typedef_global false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
     2.8 +            snd (Typedef.add_typedef_global false (Option.map Binding.name thmname)
     2.9 +              (Binding.name t, map (rpair dummyS) vs, mx) c
    2.10          (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
    2.11            | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    2.12              add_hol4_type_mapping thyname tycname true fulltyname thy
     3.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 19 00:46:08 2010 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 19 00:47:23 2010 +0100
     3.3 @@ -616,7 +616,7 @@
     3.4        thy4
     3.5        |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
     3.6            Typedef.add_typedef_global false (SOME (Binding.name name'))
     3.7 -            (Binding.name name, map fst tvs, mx)
     3.8 +            (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
     3.9              (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    3.10                 Const (cname, U --> HOLogic.boolT)) NONE
    3.11              (rtac exI 1 THEN rtac CollectI 1 THEN
     4.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 19 00:46:08 2010 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 19 00:47:23 2010 +0100
     4.3 @@ -190,7 +190,8 @@
     4.4      val (typedefs, thy3) = thy2 |>
     4.5        Sign.parent_path |>
     4.6        fold_map (fn ((((name, mx), tvs), c), name') =>
     4.7 -          Typedef.add_typedef_global false (SOME (Binding.name name')) (name, tvs, mx)
     4.8 +          Typedef.add_typedef_global false (SOME (Binding.name name'))
     4.9 +            (name, map (rpair dummyS) tvs, mx)
    4.10              (Collect $ Const (c, UnivT')) NONE
    4.11              (rtac exI 1 THEN rtac CollectI 1 THEN
    4.12                QUIET_BREADTH_FIRST (has_fewer_prems 1)
     5.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Mar 19 00:46:08 2010 +0100
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Mar 19 00:47:23 2010 +0100
     5.3 @@ -82,7 +82,7 @@
     5.4  *)
     5.5     Local_Theory.theory_result
     5.6       (Typedef.add_typedef_global false NONE
     5.7 -       (qty_name, vs, mx)
     5.8 +       (qty_name, map (rpair dummyS) vs, mx)
     5.9           (typedef_term rel rty lthy)
    5.10             NONE typedef_tac) lthy
    5.11  end
     6.1 --- a/src/HOL/Tools/typecopy.ML	Fri Mar 19 00:46:08 2010 +0100
     6.2 +++ b/src/HOL/Tools/typecopy.ML	Fri Mar 19 00:47:23 2010 +0100
     6.3 @@ -80,7 +80,8 @@
     6.4          end
     6.5    in
     6.6      thy
     6.7 -    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
     6.8 +    |> Typedef.add_typedef_global false (SOME raw_tyco)
     6.9 +      (raw_tyco, map (fn (v, _) => (v, dummyS)) vs, NoSyn)   (* FIXME keep constraints!? *)
    6.10        (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
    6.11      |-> (fn (tyco, info) => add_info tyco info)
    6.12    end;
     7.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 19 00:46:08 2010 +0100
     7.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 19 00:47:23 2010 +0100
     7.3 @@ -473,7 +473,7 @@
     7.4          val reps = map (mk_Rep_of o tfree) vs;
     7.5          val defl = list_ccomb (defl_const, reps);
     7.6          val ((_, _, _, {REP, ...}), thy) =
     7.7 -          Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy;
     7.8 +          Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
     7.9        in
    7.10          (REP, thy)
    7.11        end;