# HG changeset patch # User wenzelm # Date 1444158721 -7200 # Node ID b7e82288353586a9e4e391006cf0c8b22386fa81 # Parent 201c21438177f1f4f60615b24d8e8e77dcec202d proper context; diff -r 201c21438177 -r b7e822883535 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Oct 06 21:11:48 2015 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Tue Oct 06 21:12:01 2015 +0200 @@ -1010,27 +1010,27 @@ fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) = (case lookup consts s of - SOME ty => - let - val (t, ty') = term_of_expr thy prfx types pfuns ids e; - val T = mk_type thy prfx ty; - val T' = mk_type thy prfx ty'; - val _ = T = T' orelse - error ("Declared type " ^ ty ^ " of " ^ s ^ - "\ndoes not match type " ^ ty' ^ " in definition"); - val id' = mk_rulename id; - val lthy = Named_Target.theory_init thy; - val ((t', (_, th)), lthy') = Specification.definition - (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq - (Free (s, T), t)))) lthy; - val phi = Proof_Context.export_morphism lthy' lthy - in - ((id', Morphism.thm phi th), - ((Symtab.update (s, (Morphism.term phi t', ty)) tab, - Name.declare s ctxt), - Local_Theory.exit_global lthy')) + SOME ty => + let + val (t, ty') = term_of_expr thy prfx types pfuns ids e; + val T = mk_type thy prfx ty; + val T' = mk_type thy prfx ty'; + val _ = T = T' orelse + error ("Declared type " ^ ty ^ " of " ^ s ^ + "\ndoes not match type " ^ ty' ^ " in definition"); + val id' = mk_rulename id; + val ((t', (_, th)), lthy') = Named_Target.theory_init thy + |> Specification.definition + (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)))); + val phi = + Proof_Context.export_morphism lthy' + (Proof_Context.init_global (Proof_Context.theory_of lthy')); + in + ((id', Morphism.thm phi th), + ((Symtab.update (s, (Morphism.term phi t', ty)) tab, Name.declare s ctxt), + Local_Theory.exit_global lthy')) end - | NONE => error ("Undeclared constant " ^ s)); + | NONE => error ("Undeclared constant " ^ s)); fun add_var prfx (s, ty) (ids, thy) = let val ([Free p], ids') = mk_variables thy prfx [s] ty ids