src/Pure/Tools/find_theorems.ML
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 36950 75b8f26f2f07
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4  
     1.5  (* matching theorems *)
     1.6  
     1.7 -fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
     1.8 +fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
     1.9  
    1.10  (*educated guesses on HOL*)  (* FIXME broken *)
    1.11  val boolT = Type ("bool", []);
    1.12 @@ -110,13 +110,13 @@
    1.13      fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
    1.14      fun matches pat =
    1.15        let
    1.16 -        val jpat = ObjectLogic.drop_judgment thy pat;
    1.17 +        val jpat = Object_Logic.drop_judgment thy pat;
    1.18          val c = Term.head_of jpat;
    1.19          val pats =
    1.20            if Term.is_Const c
    1.21            then
    1.22              if doiff andalso c = iff_const then
    1.23 -              (pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat)))
    1.24 +              (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
    1.25                  |> filter (is_nontrivial thy)
    1.26              else [pat]
    1.27            else [];