src/Pure/Isar/expression.ML
changeset 45587 2f2251ec4279
parent 45290 f599ac41e7f5
child 45588 5eb47a1e4ca7
     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