# HG changeset patch # User haftmann # Date 1497938516 -7200 # Node ID 0561ac527270ed37e338db7bc3465fa73619041d # Parent 60bf6934fabd1a55f8b3c8195c7961f54d2aeef6 tuned internal signature diff -r 60bf6934fabd -r 0561ac527270 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jun 20 08:01:56 2017 +0200 +++ b/src/Pure/Isar/code.ML Tue Jun 20 08:01:56 2017 +0200 @@ -784,15 +784,17 @@ val cert_thm = Conjunction.intr_balanced (map rewrite_head thms'); in Equations (cert_thm, propers) end; -fun cert_of_proj thy c tyco = +fun cert_of_proj ctxt c tyco = let + val thy = Proof_Context.theory_of ctxt val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco; val _ = if c = rep then () else error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep); in Projection (mk_proj tyco vs ty abs rep, tyco) end; -fun cert_of_abs thy tyco c raw_abs_thm = +fun cert_of_abs ctxt tyco c raw_abs_thm = let + val thy = Proof_Context.theory_of ctxt; val abs_thm = singleton (canonize_thms thy) raw_abs_thm; val _ = assert_abs_eqn thy (SOME tyco) abs_thm; val _ = if c = const_abs_eqn thy abs_thm then () @@ -940,20 +942,16 @@ end; fun get_cert ctxt functrans c = - let - val thy = Proof_Context.theory_of ctxt; - in - case retrieve_raw thy c of - Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy - |> cert_of_eqns_preprocess ctxt functrans c - | Eqns eqns => eqns - |> cert_of_eqns_preprocess ctxt functrans c - | Unimplemented => nothing_cert ctxt c - | Proj ((_, tyco), _) => cert_of_proj thy c tyco - | Abstr ((abs_thm, tyco), _) => abs_thm - |> preprocess Conv.arg_conv ctxt - |> cert_of_abs thy tyco c - end; + case retrieve_raw (Proof_Context.theory_of ctxt) c of + Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy + |> cert_of_eqns_preprocess ctxt functrans c + | Eqns eqns => eqns + |> cert_of_eqns_preprocess ctxt functrans c + | Unimplemented => nothing_cert ctxt c + | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco + | Abstr ((abs_thm, tyco), _) => abs_thm + |> preprocess Conv.arg_conv ctxt + |> cert_of_abs ctxt tyco c; (* cases *)