# HG changeset patch # User wenzelm # Date 963523116 -7200 # Node ID 9c65fb3a7874210b5e5f4f2de6244667551dfb4d # Parent b54ebef48858328b5d35d3f23fce9fec5bd2d141 use ProofContext.bind_skolem; diff -r b54ebef48858 -r 9c65fb3a7874 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Thu Jul 13 23:17:44 2000 +0200 +++ b/src/Pure/Isar/local_defs.ML Thu Jul 13 23:18:36 2000 +0200 @@ -22,19 +22,19 @@ fun gen_def fix prep_term prep_pats raw_name atts ((x, raw_T), (raw_rhs, raw_pats)) state = let val _ = Proof.assert_forward state; + val ctxt = Proof.context_of state; (*rhs*) - val ctxt = Proof.context_of state; val name = if raw_name = "" then Thm.def_name x else raw_name; val rhs = prep_term ctxt raw_rhs; val T = Term.fastype_of rhs; val pats = prep_pats T (ProofContext.declare_term rhs ctxt) raw_pats; (*lhs*) - val state' = fix [([x], raw_T)] state; - val lhs = ProofContext.intern_skolem (Proof.context_of state') (Free (x, T)); + val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T)); in - state' + state + |> fix [([x], raw_T)] |> Proof.match_bind_i [(pats, rhs)] |> Proof.assm_i (refl_tac, refl_tac) [(name, atts, [(Logic.mk_equals (lhs, rhs), ([], []))])] end;