equal
deleted
inserted
replaced
282 (*the same name are renamed during printing*) |
282 (*the same name are renamed during printing*) |
283 |
283 |
284 val (param_names, ctxt') = ctxt |
284 val (param_names, ctxt') = ctxt |
285 |> Variable.declare_thm thm |
285 |> Variable.declare_thm thm |
286 |> Thm.fold_terms Variable.declare_constraints st |
286 |> Thm.fold_terms Variable.declare_constraints st |
287 |> ProofContext.add_fixes_i (map (fn (x, T) => (x, SOME T, NoSyn)) params); |
287 |> ProofContext.add_fixes_i (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) params); |
288 |
288 |
289 (* Process type insts: Tinsts_env *) |
289 (* Process type insts: Tinsts_env *) |
290 fun absent xi = error |
290 fun absent xi = error |
291 ("No such variable in theorem: " ^ Term.string_of_vname xi); |
291 ("No such variable in theorem: " ^ Term.string_of_vname xi); |
292 val (rtypes, rsorts) = Drule.types_sorts thm; |
292 val (rtypes, rsorts) = Drule.types_sorts thm; |