src/Pure/sign.ML
changeset 155 f58571828c68
parent 143 f8152ca36cd5
child 169 1b2765146aab
     1.1 --- a/src/Pure/sign.ML	Thu Nov 25 15:32:42 1993 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 25 19:09:43 1993 +0100
     1.3 @@ -138,16 +138,16 @@
     1.4    it is impossible to forge a signature. *)
     1.5  
     1.6  fun extend (Sg {tsig, const_tab, syn, stamps}) signame
     1.7 -  (newclasses, newdefault, otypes, newtypes, const_decs, osext) =
     1.8 +  (classes, default, types, arities, const_decs, osext) =
     1.9    let
    1.10      (* FIXME abbr *)
    1.11 -    val tsig' = Type.extend (tsig, newclasses, newdefault, otypes, newtypes);
    1.12 +    val tsig' = Type.extend (tsig, classes, default, types, arities);
    1.13  
    1.14      (* FIXME expand_typ, check typ *)
    1.15      val read_ty = Syntax.read_typ syn (K (Type.defaultS tsig'));
    1.16  
    1.17 -    val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 newtypes)));
    1.18 -    val xconsts = map #1 newclasses @ flat (map #1 otypes) @ flat (map #1 const_decs);
    1.19 +    val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 arities)));
    1.20 +    val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
    1.21      val syn' =
    1.22        (case osext of
    1.23          Some sext => Syntax.extend syn read_ty (roots, xconsts, sext)
    1.24 @@ -185,8 +185,7 @@
    1.25    (Syntax.syntax_types, 0)],
    1.26   [(["fun"],  ([["logic"], ["logic"]], "logic")),
    1.27    (["prop"], ([], "logic"))],
    1.28 - [(["*NORMALIZED*"], "'a::{} => 'a"),
    1.29 -  ([Syntax.constrainC], "'a::logic => 'a")],  (* MMW FIXME replace logic by {} (?) *)
    1.30 + [([Syntax.constrainC], "'a::logic => 'a")],  (* MMW FIXME replace logic by {} (?) *)
    1.31   Some Syntax.pure_sext);
    1.32  
    1.33