author | wenzelm |
Tue, 07 Sep 1999 16:57:52 +0200 | |
changeset 7505 | a9690e9cc58a |
parent 7504 | 0fec51813079 |
child 7506 | 08a88d4ebd54 |
--- 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));