1.1 --- a/src/Pure/Isar/rule_insts.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -284,7 +284,7 @@
     1.4          val (param_names, ctxt') = ctxt
     1.5            |> Variable.declare_thm thm
     1.6            |> Thm.fold_terms Variable.declare_constraints st
     1.7 -          |> ProofContext.add_fixes_i (map (fn (x, T) => (x, SOME T, NoSyn)) params);
     1.8 +          |> ProofContext.add_fixes_i (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) params);
     1.9  
    1.10          (* Process type insts: Tinsts_env *)
    1.11          fun absent xi = error