changeset 28965 | 1de908189869 |
parent 28083 | 103d9282a946 |
child 29606 | fedb8be05f24 |
--- a/src/Pure/Isar/rule_insts.ML Wed Dec 03 21:00:39 2008 -0800 +++ b/src/Pure/Isar/rule_insts.ML Thu Dec 04 14:43:33 2008 +0100 @@ -284,7 +284,7 @@ val (param_names, ctxt') = ctxt |> Variable.declare_thm thm |> Thm.fold_terms Variable.declare_constraints st - |> ProofContext.add_fixes_i (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) params); + |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params); (* Process type insts: Tinsts_env *) fun absent xi = error