re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
authorwenzelm
Fri Apr 29 01:21:44 2016 +0200 (2016-04-29 ago)
changeset 63069f009347b9072
parent 63068 8b9401bfd9fd
child 63070 952714a20087
re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Apr 28 15:42:52 2016 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Apr 29 01:21:44 2016 +0200
     1.3 @@ -101,14 +101,16 @@
     1.4  local
     1.5  
     1.6  fun close_forms ctxt auto_close i prems concls =
     1.7 -  let
     1.8 -    val xs =
     1.9 -      if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) [])
    1.10 -      else [];
    1.11 -    val types =
    1.12 -      map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
    1.13 -    val uniform_typing = AList.lookup (op =) (xs ~~ types);
    1.14 -  in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
    1.15 +  if not auto_close andalso null prems then concls
    1.16 +  else
    1.17 +    let
    1.18 +      val xs =
    1.19 +        if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) [])
    1.20 +        else [];
    1.21 +      val types =
    1.22 +        map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
    1.23 +      val uniform_typing = AList.lookup (op =) (xs ~~ types);
    1.24 +    in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
    1.25  
    1.26  fun get_positions ctxt x =
    1.27    let