clarified order: params/prems/concl interchangeable with !!/==> proposition;
authorwenzelm
Thu, 28 Apr 2016 11:31:36 +0200
changeset 63065 3cb7b06d0a9f
parent 63064 2f18172214c8
child 63066 4b0ad6c5d1ca
clarified order: params/prems/concl interchangeable with !!/==> proposition;
src/Pure/Isar/specification.ML
--- 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));