src/Pure/Isar/find_theorems.ML
changeset 22709 9ab51bac6287
parent 22414 3f189ea9bfe7
child 24683 c62320337a4e
     1.1 --- a/src/Pure/Isar/find_theorems.ML	Sun Apr 15 23:25:49 2007 +0200
     1.2 +++ b/src/Pure/Isar/find_theorems.ML	Sun Apr 15 23:25:50 2007 +0200
     1.3 @@ -28,9 +28,9 @@
     1.4    | read_criterion _ Elim = Elim
     1.5    | read_criterion _ Dest = Dest
     1.6    | read_criterion ctxt (Simp str) =
     1.7 -      Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
     1.8 +      Simp (hd (ProofContext.read_term_pats dummyT ctxt [str]))
     1.9    | read_criterion ctxt (Pattern str) =
    1.10 -      Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
    1.11 +      Pattern (hd (ProofContext.read_term_pats dummyT ctxt [str]));
    1.12  
    1.13  fun pretty_criterion ctxt (b, c) =
    1.14    let