src/Pure/Isar/proof_context.ML
changeset 7505 a9690e9cc58a
parent 7486 1f9eceb434db
child 7557 1b977741f530
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 07 16:57:28 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 07 16:57:52 1999 +0200
     1.3 @@ -330,7 +330,7 @@
     1.4  
     1.5  
     1.6  fun read_term_sg freeze sg (defs as (_, _, used)) s =
     1.7 -  #1 (read_def_termT freeze sg defs (s, TVar ((variant used "'z", 0), logicS)));
     1.8 +  #1 (read_def_termT freeze sg defs (s, dummyT));
     1.9  
    1.10  fun read_prop_sg freeze sg defs s =
    1.11    #1 (read_def_termT freeze sg defs (s, propT));