--- 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