# HG changeset patch
# User wenzelm
# Date 1175621056 -7200
# Node ID f166a5416b3fd8b8313bf03062c1250ef05c6e14
# Parent  e5d7d9de7d856eda017318a8d7c58c09f7a3b511
renamed of_sort_derivation record fields (avoid clash with Alice keywords);

diff -r e5d7d9de7d85 -r f166a5416b3f src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Tue Apr 03 19:24:15 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Tue Apr 03 19:24:16 2007 +0200
@@ -89,17 +89,18 @@
   let
     val tys_decl = Sign.const_typargs thy (c, ty_decl);
     val tys = Sign.const_typargs thy (c, ty);
-    fun classrel (x, _) _ = x;
-    fun constructor tyco xs class =
+    fun class_relation (x, _) _ = x;
+    fun type_constructor tyco xs class =
       (tyco, class) :: maps (maps fst) xs;
-    fun variable (TVar (_, sort)) = map (pair []) sort
-      | variable (TFree (_, sort)) = map (pair []) sort;
+    fun type_variable (TVar (_, sort)) = map (pair []) sort
+      | type_variable (TFree (_, sort)) = map (pair []) sort;
     fun mk_inst ty (TVar (_, sort)) = cons (ty, sort)
       | mk_inst ty (TFree (_, sort)) = cons (ty, sort)
       | mk_inst (Type (_, tys1)) (Type (_, tys2)) = fold2 mk_inst tys1 tys2;
     fun of_sort_deriv (ty, sort) =
       Sorts.of_sort_derivation (Sign.pp thy) algebra
-        { classrel = classrel, constructor = constructor, variable = variable }
+        { class_relation = class_relation, type_constructor = type_constructor,
+          type_variable = type_variable }
         (ty, sort)
   in
     flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl []))
diff -r e5d7d9de7d85 -r f166a5416b3f src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Tue Apr 03 19:24:15 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Tue Apr 03 19:24:16 2007 +0200
@@ -210,18 +210,19 @@
     datatype typarg =
         Global of (class * string) * typarg list list
       | Local of (class * class) list * (string * (int * sort));
-    fun classrel (Global ((_, tyco), yss), _) class =
+    fun class_relation (Global ((_, tyco), yss), _) class =
           Global ((class, tyco), yss)
-      | classrel (Local (classrels, v), subclass) superclass =
+      | class_relation (Local (classrels, v), subclass) superclass =
           Local ((subclass, superclass) :: classrels, v);
-    fun constructor tyco yss class =
+    fun type_constructor tyco yss class =
       Global ((class, tyco), (map o map) fst yss);
-    fun variable (TFree (v, sort)) =
+    fun type_variable (TFree (v, sort)) =
       let
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
     val typargs = Sorts.of_sort_derivation pp algebra
-      {classrel = classrel, constructor = constructor, variable = variable}
+      {class_relation = class_relation, type_constructor = type_constructor,
+       type_variable = type_variable}
       (ty_ctxt, proj_sort sort_decl);
     fun mk_dict (Global (inst, yss)) =
           ensure_def_inst thy algbr funcgr strct inst
diff -r e5d7d9de7d85 -r f166a5416b3f src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Apr 03 19:24:15 2007 +0200
+++ b/src/Pure/axclass.ML	Tue Apr 03 19:24:16 2007 +0200
@@ -436,13 +436,13 @@
         val hyps = vars
           |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
         val ths = (typ, sort) |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy)
-           {classrel =
+           {class_relation =
               fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
-            constructor =
+            type_constructor =
               fn a => fn dom => fn c =>
                 let val Ss = map (map snd) dom and ths = maps (map fst) dom
                 in ths MRS the_arity thy a (c, Ss) end,
-            variable =
+            type_variable =
               the_default [] o AList.lookup (op =) hyps};
       in ths end;
 
diff -r e5d7d9de7d85 -r f166a5416b3f src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Tue Apr 03 19:24:15 2007 +0200
+++ b/src/Pure/sorts.ML	Tue Apr 03 19:24:16 2007 +0200
@@ -52,9 +52,9 @@
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool
   val of_sort_derivation: Pretty.pp -> algebra ->
-    {classrel: 'a * class -> class -> 'a,
-     constructor: string -> ('a * class) list list -> class -> 'a,
-     variable: typ -> ('a * class) list} ->
+    {class_relation: 'a * class -> class -> 'a,
+     type_constructor: string -> ('a * class) list list -> class -> 'a,
+     type_variable: typ -> ('a * class) list} ->
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
   val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
 end;
@@ -348,11 +348,11 @@
 
 (* of_sort_derivation *)
 
-fun of_sort_derivation pp algebra {classrel, constructor, variable} =
+fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
   let
     val {classes, arities} = rep_algebra algebra;
     fun weaken_path (x, c1 :: c2 :: cs) =
-          weaken_path (classrel (x, c1) c2, c2 :: cs)
+          weaken_path (class_relation (x, c1) c2, c2 :: cs)
       | weaken_path (x, _) = x;
     fun weaken (x, c1) c2 =
       (case Graph.irreducible_paths classes (c1, c2) of
@@ -375,9 +375,9 @@
               let
                 val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
                 val dom' = map2 (fn d => fn S' => weakens d S' ~~ S') dom Ss';
-              in weaken (constructor a dom' c0, c0) c end)
+              in weaken (type_constructor a dom' c0, c0) c end)
           end
-      | derive T S = weakens (variable T) S;
+      | derive T S = weakens (type_variable T) S;
   in uncurry derive end;