src/Pure/goals.ML

--- a/src/Pure/goals.ML	Tue Jan 04 17:05:43 2000 +0100
+++ b/src/Pure/goals.ML	Wed Jan 05 11:35:18 2000 +0100
@@ -541,8 +541,7 @@
 
 fun top_sg() = #sign(rep_thm(topthm()));
 
-fun read s = term_of (read_cterm (top_sg())
-			                   (s, (TVar(("DUMMY",0),[]))));
+fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
 
 (*Print a term under the current signature of the proof state*)
 fun prin t = writeln (Sign.string_of_term (top_sg()) t);