author | wenzelm |
Thu, 28 Apr 2016 11:31:36 +0200 | |
changeset 63065 | 3cb7b06d0a9f |
parent 63064 | 2f18172214c8 |
child 63066 | 4b0ad6c5d1ca |
--- a/src/Pure/Isar/specification.ML Thu Apr 28 09:43:11 2016 +0200 +++ b/src/Pure/Isar/specification.ML Thu Apr 28 11:31:36 2016 +0200 @@ -103,7 +103,7 @@ fun close_forms ctxt auto_close i prems concls = let val xs = - if auto_close then rev (fold (Variable.add_free_names ctxt) (concls @ prems) []) + if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) []) else []; val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));