clarified order: params/prems/concl interchangeable with !!/==> proposition;
authorwenzelm
Thu Apr 28 11:31:36 2016 +0200 (2016-04-28 ago)
changeset 630653cb7b06d0a9f
parent 63064 2f18172214c8
child 63066 4b0ad6c5d1ca
clarified order: params/prems/concl interchangeable with !!/==> proposition;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Apr 28 09:43:11 2016 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Apr 28 11:31:36 2016 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  fun close_forms ctxt auto_close i prems concls =
     1.5    let
     1.6      val xs =
     1.7 -      if auto_close then rev (fold (Variable.add_free_names ctxt) (concls @ prems) [])
     1.8 +      if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) [])
     1.9        else [];
    1.10      val types =
    1.11        map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));