# HG changeset patch
# User wenzelm
# Date 936716272 -7200
# Node ID a9690e9cc58aa4596e1cd4ce95ec3f0610c5b5ea
# Parent  0fec518130794220be2167fd11a970b1c3f1b6c6
read_def_termT: dummyT;

diff -r 0fec51813079 -r a9690e9cc58a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Sep 07 16:57:28 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 07 16:57:52 1999 +0200
@@ -330,7 +330,7 @@
 
 
 fun read_term_sg freeze sg (defs as (_, _, used)) s =
-  #1 (read_def_termT freeze sg defs (s, TVar ((variant used "'z", 0), logicS)));
+  #1 (read_def_termT freeze sg defs (s, dummyT));
 
 fun read_prop_sg freeze sg defs s =
   #1 (read_def_termT freeze sg defs (s, propT));