# HG changeset patch
# User haftmann
# Date 1192815931 -7200
# Node ID 1ee419a5a30f27fd1a814bc2318cfecd5d3f732a
# Parent  db3e412c4cb19fc3f3c30889a7d32c27c9a61a9a
tuned

diff -r db3e412c4cb1 -r 1ee419a5a30f src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Oct 19 19:45:29 2007 +0200
+++ b/src/HOL/Orderings.thy	Fri Oct 19 19:45:31 2007 +0200
@@ -114,7 +114,7 @@
 text {* Reverse order *}
 
 lemma order_reverse:
-  "order (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
+  "order (op \<ge>) (op >)"
 by unfold_locales
    (simp add: less_le, auto intro: antisym order_trans)
 
@@ -187,7 +187,7 @@
 text {* Reverse order *}
 
 lemma linorder_reverse:
-  "linorder (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
+  "linorder (op \<ge>) (op >)"
 by unfold_locales
   (simp add: less_le, auto intro: antisym order_trans simp add: linear)
 
@@ -597,15 +597,6 @@
 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
 
-lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
-lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
-lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
-lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
-lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
-lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
-lemmas split_min = linorder_class.split_min
-lemmas split_max = linorder_class.split_max
-
 
 subsection {* Bounded quantifiers *}
 
diff -r db3e412c4cb1 -r 1ee419a5a30f src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Oct 19 19:45:29 2007 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 19 19:45:31 2007 +0200
@@ -664,7 +664,7 @@
   |> synchronize_syntax thy sups base_sort
   |> Context.proof_map (
       Syntax.add_term_check 0 "class" sort_term_check
-      #> Syntax.add_term_uncheck (~10) "class" sort_term_uncheck)
+      #> Syntax.add_term_uncheck 0 "class" sort_term_uncheck)
 
 fun init class ctxt =
   let
@@ -821,8 +821,6 @@
     thy'
     |> Sign.hide_consts_i false [c''] (*FIXME*)
     |> Sign.declare_const pos (c, ty'', mx) |> snd
-    |> Sign.parent_path
-    |> Sign.sticky_prefix prfx
     |> Thm.add_def false (c, def_eq)
     |>> Thm.symmetric
     |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
@@ -847,14 +845,19 @@
       |> map (Pattern.rewrite_term thy rews []);
   in Term.betapplys (head', ts') end;
 
-fun add_syntactic_const class prmode pos ((c, mx), dict) thy =
+fun fold_aux_defs thy class =
+  let
+    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy [class])
+  in Pattern.rewrite_term thy rews [] end;
+
+fun add_syntactic_const class prmode pos ((c, mx), rhs) thy =
   let
     val prfx = class_prefix class;
     val thy' = thy |> Sign.add_path prfx;
     val phi = morphism thy class;
 
     val c' = Sign.full_name thy' c;
-    val dict' = (expand_aux_abbrev thy' class o Morphism.term phi) dict;
+    val dict' = (expand_aux_abbrev thy' class o Morphism.term phi) rhs;
     val dict'' = map_types Logic.unvarifyT dict';
     val ty' = Term.fastype_of dict'';
 
@@ -867,7 +870,7 @@
     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts dict') |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
-    |> register_operation class ((c', (dict, dict'')), NONE)
+    |> register_operation class ((c', (dict', dict'')), NONE)
     |> Sign.restore_naming thy
     |> pair c'
   end;
diff -r db3e412c4cb1 -r 1ee419a5a30f src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Fri Oct 19 19:45:29 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML	Fri Oct 19 19:45:31 2007 +0200
@@ -302,7 +302,7 @@
     val drop = drop_classes thy tfrees;
     val instdefs = instances_of_consts thy algebra funcgr' c_exprs;
     val funcgr'' = ensure_consts thy algebra instdefs funcgr';
-  in (f drop thm5 funcgr'' ct'' , funcgr'') end;
+  in (f drop thm5 funcgr'' ct'', funcgr'') end;
 
 fun raw_eval_conv thy conv =
   let