--- a/src/Pure/Tools/find_theorems.ML Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Tools/find_theorems.ML Sun Mar 07 12:19:47 2010 +0100
@@ -93,7 +93,7 @@
(* matching theorems *)
-fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
+fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
(*educated guesses on HOL*) (* FIXME broken *)
val boolT = Type ("bool", []);
@@ -110,13 +110,13 @@
fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
fun matches pat =
let
- val jpat = ObjectLogic.drop_judgment thy pat;
+ val jpat = Object_Logic.drop_judgment thy pat;
val c = Term.head_of jpat;
val pats =
if Term.is_Const c
then
if doiff andalso c = iff_const then
- (pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat)))
+ (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
|> filter (is_nontrivial thy)
else [pat]
else [];