# HG changeset patch
# User nipkow
# Date 754250983 -3600
# Node ID f58571828c6852e2fd7f796413f84033db75895d
# Parent  f8c3715457b80fcce276d89b1ac5ac4a77bb32cc
changed some names and deleted *NORMALIZED*

diff -r f8c3715457b8 -r f58571828c68 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Nov 25 15:32:42 1993 +0100
+++ b/src/Pure/sign.ML	Thu Nov 25 19:09:43 1993 +0100
@@ -138,16 +138,16 @@
   it is impossible to forge a signature. *)
 
 fun extend (Sg {tsig, const_tab, syn, stamps}) signame
-  (newclasses, newdefault, otypes, newtypes, const_decs, osext) =
+  (classes, default, types, arities, const_decs, osext) =
   let
     (* FIXME abbr *)
-    val tsig' = Type.extend (tsig, newclasses, newdefault, otypes, newtypes);
+    val tsig' = Type.extend (tsig, classes, default, types, arities);
 
     (* FIXME expand_typ, check typ *)
     val read_ty = Syntax.read_typ syn (K (Type.defaultS tsig'));
 
-    val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 newtypes)));
-    val xconsts = map #1 newclasses @ flat (map #1 otypes) @ flat (map #1 const_decs);
+    val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 arities)));
+    val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
     val syn' =
       (case osext of
         Some sext => Syntax.extend syn read_ty (roots, xconsts, sext)
@@ -185,8 +185,7 @@
   (Syntax.syntax_types, 0)],
  [(["fun"],  ([["logic"], ["logic"]], "logic")),
   (["prop"], ([], "logic"))],
- [(["*NORMALIZED*"], "'a::{} => 'a"),
-  ([Syntax.constrainC], "'a::logic => 'a")],  (* MMW FIXME replace logic by {} (?) *)
+ [([Syntax.constrainC], "'a::logic => 'a")],  (* MMW FIXME replace logic by {} (?) *)
  Some Syntax.pure_sext);