# HG changeset patch
# User haftmann
# Date 1193203192 -7200
# Node ID f737a88a3248fc0cfb70125ebd71ea4a4c8f5e94
# Parent  ad4d5365d9d871a130272101b21fec4fc91e4f5c
tuned

diff -r ad4d5365d9d8 -r f737a88a3248 NEWS
--- a/NEWS	Tue Oct 23 23:27:23 2007 +0200
+++ b/NEWS	Wed Oct 24 07:19:52 2007 +0200
@@ -823,7 +823,7 @@
 package; constants add, mul, pow now curried.  Infix syntax for
 algebraic operations.
 
-* Some steps towards more uniform lattice theory development in HOL.
+* More uniform lattice theory development in HOL.
 
     constants "meet" and "join" now named "inf" and "sup"
     constant "Meet" now named "Inf"
@@ -946,6 +946,9 @@
 * Classes "order" and "linorder": potential INCOMPATIBILITY due to
 changed order of proof goals instance proofs.
 
+* Locale "partial_order" now unified with class "order" (cf. theory
+Orderings), added parameter "less".  INCOMPATIBILITY.
+
 * Dropped redundant lemma def_imp_eq in favor of meta_eq_to_obj_eq.
 INCOMPATIBILITY.
 
@@ -977,10 +980,7 @@
 
 * Class "recpower" is generalized to arbitrary monoids, not just
 commutative semirings.  INCOMPATIBILITY: may need to incorporate
-commutativity or a semiring properties additionally.
-
-* Unified locale "partial_order" with class definition (cf. theory
-Orderings), added parameter "less".  INCOMPATIBILITY.
+commutativity or semiring properties additionally.
 
 * Constant "List.list_all2" in List.thy now uses authentic syntax.
 INCOMPATIBILITY: translations containing list_all2 may go wrong,
@@ -1005,11 +1005,12 @@
 
 See HOL/Integ/IntArith.thy for an example setup.
 
-* New top level command 'normal_form' computes the normal form of a
-term that may contain free variables.  For example ``normal_form
-"rev[a,b,c]"'' produces ``[b,c,a]'' (without proof).  This command is
-suitable for heavy-duty computations because the functions are
-compiled to ML first.
+* Command 'normal_form' computes the normal form of a
+term that may contain free variables.  For example
+``normal_form "rev [a, b, c]"'' produces ``[b, c, a]'' (without proof).
+This command is suitable for heavy-duty computations because the functions
+are compiled to ML first.  Correspondingly, a method ``normalization''
+is provided.  See further HOL/ex/NormalForm.thy and Tools/nbe.ML.
 
 * Alternative iff syntax "A <-> B" for equality on bool (with priority
 25 like -->); output depends on the "iff" print_mode, the default is
diff -r ad4d5365d9d8 -r f737a88a3248 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Oct 23 23:27:23 2007 +0200
+++ b/src/Pure/Isar/class.ML	Wed Oct 24 07:19:52 2007 +0200
@@ -433,16 +433,13 @@
 
 (* updaters *)
 
-fun add_class_data ((class, superclasses), (cs, base_sort, insttab, phi, intro)) thy =
+fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
   let
-    val inst = map
-      (SOME o the o Symtab.lookup insttab o fst o fst)
-        (Locale.parameters_of_expr thy (Locale.Locale class));
     val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
       (c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs;
     val cs = (map o pairself) fst cs;
     val add_class = Graph.new_node (class,
-        mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations)))
+        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
       #> fold (curry Graph.add_edge class) superclasses;
   in
     ClassData.map add_class thy
@@ -738,10 +735,8 @@
     val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
       prep_spec thy raw_supclasses raw_includes_elems;
     val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
-    fun mk_inst class param_names cs =
-      Symtab.empty
-      |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
-           (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
+    fun mk_inst class cs =
+      (map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs;
     fun fork_syntax (Element.Fixes xs) =
           fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
           #>> Element.Fixes
@@ -785,7 +780,7 @@
       #-> (fn [(_, [class_intro])] =>
         add_class_data ((class, sups),
           (map fst params ~~ consts, base_sort,
-            mk_inst class (map fst all_params) (map snd supconsts @ consts),
+            mk_inst class (map snd supconsts @ consts),
               calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
       #> class_interpretation class axioms []
       )))))