--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Sep 12 13:42:28 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Sep 12 13:56:49 2012 +0200
@@ -38,7 +38,7 @@
end
fun pred_of_function thy name =
- case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of
+ case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
[] => NONE
| [(f, p)] => SOME (fst (dest_Const p))
| _ => error ("Multiple matches possible for lookup of constant " ^ name)