# HG changeset patch
# User wenzelm
# Date 1190579004 -7200
# Node ID 5b168969ffe0e7a378afa93cff8f8d910cf7e987
# Parent  232e71c2a6d9f3574fa01866e844bc4b42a5f3a1
tuned ML setup;

diff -r 232e71c2a6d9 -r 5b168969ffe0 src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Sun Sep 23 22:11:50 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Sun Sep 23 22:23:24 2007 +0200
@@ -504,8 +504,7 @@
 fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
 fun generic_whatis phi =
  let
-  val [lt, le] = map (Morphism.term phi)
-   (ProofContext.read_term_pats dummyT @{context} ["op \<sqsubset>", "op \<sqsubseteq>"]) (* FIXME avoid read? *)
+  val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
   fun h x t =
    case term_of t of
      Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq