tuned;
authorwenzelm
Sat Nov 19 15:04:36 2011 +0100 (2011-11-19)
changeset 455872f2251ec4279
parent 45586 c94f149cdf5d
child 45588 5eb47a1e4ca7
tuned;
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Nov 19 14:31:43 2011 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Nov 19 15:04:36 2011 +0100
     1.3 @@ -354,8 +354,9 @@
     1.4        let
     1.5          val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
     1.6          val inst' = prep_inst ctxt parm_names inst;
     1.7 -        val parm_types' = map (Type_Infer.paramify_vars o
     1.8 -          Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
     1.9 +        val parm_types' = parm_types
    1.10 +          |> map (Type_Infer.paramify_vars o
    1.11 +              Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
    1.12          val inst'' = map2 Type.constraint parm_types' inst';
    1.13          val insts' = insts @ [(loc, (prfx, inst''))];
    1.14          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
    1.15 @@ -836,7 +837,7 @@
    1.16        |> prep_expr expression;
    1.17      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.18  
    1.19 -    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
    1.20 +    val attrss = map (apsnd (map (prep_attr theory)) o fst) equations;
    1.21      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.22      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.23  
    1.24 @@ -856,7 +857,7 @@
    1.25      val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
    1.26      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.27  
    1.28 -    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
    1.29 +    val attrss = map (apsnd (map (prep_attr theory)) o fst) equations;
    1.30      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.31      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.32  
    1.33 @@ -915,7 +916,7 @@
    1.34      val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    1.35      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.36  
    1.37 -    val attrss = map ((apsnd o map) (prep_attr thy) o fst) equations;
    1.38 +    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
    1.39      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.40      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.41  
     2.1 --- a/src/Pure/Isar/locale.ML	Sat Nov 19 14:31:43 2011 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Sat Nov 19 15:04:36 2011 +0100
     2.3 @@ -462,7 +462,8 @@
     2.4  fun activate_facts export dep context =
     2.5    let
     2.6      val thy = Context.theory_of context;
     2.7 -    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
     2.8 +    val activate =
     2.9 +      activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
    2.10    in
    2.11      roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
    2.12        dep (get_idents context, context)
    2.13 @@ -688,7 +689,7 @@
    2.14      fun add_locale_deps name =
    2.15        let
    2.16          val dependencies =
    2.17 -          (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name |> map fst);
    2.18 +          map (apsnd (instance_of thy name o op $>) o fst) (dependencies_of thy name);
    2.19        in
    2.20          fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
    2.21            deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))