1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Sep 30 19:04:48 2009 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Sep 30 22:20:58 2009 +0200
     1.3 @@ -1033,7 +1033,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
     1.8 +fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
     1.9    | const_syntax ctxt (Const (c, _), mx) =
    1.10        Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
    1.11    | const_syntax _ _ = NONE;
    1.12 @@ -1106,7 +1106,7 @@
    1.13  
    1.14  (* fixes vs. frees *)
    1.15  
    1.16 -fun auto_fixes (arg as (ctxt, (propss, x))) =
    1.17 +fun auto_fixes (ctxt, (propss, x)) =
    1.18    ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
    1.19  
    1.20  fun bind_fixes xs ctxt =