# HG changeset patch
# User wenzelm
# Date 1187126569 -7200
# Node ID f53b7dab4426e222775f18a792c3b920c1f24e4d
# Parent  4b2aac7669b3452d942a60912690f42cca613177
fixed dummyT (used as constraint);

diff -r 4b2aac7669b3 -r f53b7dab4426 src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Tue Aug 14 23:05:55 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Tue Aug 14 23:22:49 2007 +0200
@@ -520,7 +520,7 @@
 fun generic_whatis phi =
  let
   val [lt, le] = map (Morphism.term phi)
-   (ProofContext.read_term_pats @{typ "dummy"} @{context} ["op \<sqsubset>", "op \<sqsubseteq>"]) (* FIXME avoid read? *)
+   (ProofContext.read_term_pats dummyT @{context} ["op \<sqsubset>", "op \<sqsubseteq>"]) (* FIXME avoid read? *)
   fun h x t =
    case term_of t of
      Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq