src/Pure/sign.ML
changeset 22709 9ab51bac6287
parent 22696 00fc658c4fe5
child 22765 2a3840aa2ffd
     1.1 --- a/src/Pure/sign.ML	Sun Apr 15 23:25:49 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Apr 15 23:25:50 2007 +0200
     1.3 @@ -610,7 +610,7 @@
     1.4  
     1.5      val args = sTs |> map (fn (s, raw_T) =>
     1.6        let val T = certify_typ thy raw_T handle TYPE (msg, _, _) => error msg
     1.7 -      in (read T s, T) end);
     1.8 +      in (read (#1 (TypeInfer.paramify_dummies T 0)) s, T) end);
     1.9  
    1.10      (*brute-force disambiguation via type-inference*)
    1.11      val termss = fold_rev (multiply o fst) args [[]];
    1.12 @@ -655,7 +655,7 @@
    1.13    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
    1.14    in t end handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
    1.15  
    1.16 -fun read_term thy = simple_read_term thy TypeInfer.logicT;
    1.17 +fun read_term thy = simple_read_term thy dummyT;
    1.18  fun read_prop thy = simple_read_term thy propT;
    1.19  
    1.20