src/Pure/Isar/proof_context.ML
changeset 62768 5f5f11ee4d37
parent 62767 d6b0d35b3aed
child 62773 e6443edaebff
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 30 20:56:39 2016 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 30 21:16:22 2016 +0200
     1.3 @@ -1060,7 +1060,7 @@
     1.4  
     1.5  fun declare_var (x, opt_T, mx) ctxt =
     1.6    let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx)
     1.7 -  in ((x, T, mx), ctxt |> Variable.declare_constraints (Free (x, T))) end;
     1.8 +  in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
     1.9  
    1.10  fun add_syntax vars ctxt =
    1.11    map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt;
    1.12 @@ -1076,11 +1076,10 @@
    1.13  
    1.14  local
    1.15  
    1.16 -fun check_mixfix ctxt (b, opt_T, mx) =
    1.17 +fun check_mixfix ctxt (b, T, mx) =
    1.18    let
    1.19      val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt;
    1.20      val mx' = Mixfix.reset_pos mx;
    1.21 -    val T = #2 (#1 (declare_var (x, opt_T, mx') ctxt));
    1.22      val _ = add_syntax [(x, T, if Context_Position.is_visible ctxt then mx else mx')] ctxt';
    1.23    in mx' end;
    1.24  
    1.25 @@ -1091,9 +1090,9 @@
    1.26        if internal then T
    1.27        else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
    1.28      val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
    1.29 -    val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt (b, opt_T, mx);
    1.30 -    val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx');
    1.31 -  in ((b, opt_T, mx'), ctxt') end;
    1.32 +    val (T, ctxt') = ctxt |> declare_var (x, opt_T, mx);
    1.33 +    val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt' (b, T, mx);
    1.34 +  in ((b, SOME T, mx'), ctxt') end;
    1.35  
    1.36  in
    1.37  
    1.38 @@ -1194,12 +1193,10 @@
    1.39    let
    1.40      val (vars, _) = fold_map prep_var raw_vars ctxt;
    1.41      val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
    1.42 -  in
    1.43 -    ctxt'
    1.44 -    |> fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
    1.45 -    |-> add_syntax
    1.46 -    |> pair xs
    1.47 -  end;
    1.48 +    val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars;
    1.49 +    val (Ts, ctxt'') = fold_map declare_var vars' ctxt';
    1.50 +    val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars';
    1.51 +  in (xs, add_syntax vars'' ctxt'') end;
    1.52  
    1.53  in
    1.54