src/Pure/Isar/rule_insts.ML
changeset 28965 1de908189869
parent 28083 103d9282a946
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Dec 04 14:43:33 2008 +0100
     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) => (Name.binding x, SOME T, NoSyn)) params);
     1.8 +          |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
     1.9  
    1.10          (* Process type insts: Tinsts_env *)
    1.11          fun absent xi = error