PureThy.add_typedecls;
authorwenzelm
Fri May 15 11:34:12 1998 +0200 (1998-05-15)
changeset 4932c90411dde8e8
parent 4931 2ec84dee7911
child 4933 c85b339accfe
PureThy.add_typedecls;
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu May 14 16:54:20 1998 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri May 15 11:34:12 1998 +0200
     1.3 @@ -59,7 +59,6 @@
     1.4        map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
     1.5  
     1.6      val tname = Syntax.type_name t mx;
     1.7 -    val tlen = length vs;
     1.8      val newT = Type (full_name tname, map TFree lhs_tfrees);
     1.9  
    1.10      val Rep_name = "Rep_" ^ name;
    1.11 @@ -106,10 +105,9 @@
    1.12      prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
    1.13  
    1.14      thy
    1.15 -    |> Theory.add_types [(t, tlen, mx)]
    1.16 +    |> PureThy.add_typedecls [(t, vs, mx)]
    1.17      |> Theory.add_arities_i
    1.18 -     [(full_name tname, replicate tlen logicS, logicS),
    1.19 -      (full_name tname, replicate tlen HOLogic.termS, HOLogic.termS)]
    1.20 +     [(full_name tname, replicate (length vs) HOLogic.termS, HOLogic.termS)]
    1.21      |> Theory.add_consts_i
    1.22       [(name, setT, NoSyn),
    1.23        (Rep_name, newT --> oldT, NoSyn),