# HG changeset patch # User wenzelm # Date 1129327684 -7200 # Node ID 64c832a03a15c9a392882e572d772141279be314 # Parent 44b6dde80bf4bbb13424f2cad7410c0071847390 goal statements: accomodate before_qed argument; diff -r 44b6dde80bf4 -r 64c832a03a15 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Sat Oct 15 00:08:03 2005 +0200 +++ b/src/Pure/Isar/isar_thy.ML Sat Oct 15 00:08:04 2005 +0200 @@ -102,10 +102,10 @@ local fun local_goal opt_chain goal stmt int = - opt_chain #> goal (K (K Seq.single)) stmt int; + opt_chain #> goal NONE (K (K Seq.single)) stmt int; fun global_goal goal kind a propp thy = - goal kind (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy); + goal kind NONE (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy); in diff -r 44b6dde80bf4 -r 64c832a03a15 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sat Oct 15 00:08:03 2005 +0200 +++ b/src/Pure/axclass.ML Sat Oct 15 00:08:04 2005 +0200 @@ -315,7 +315,7 @@ fun gen_instance mk_prop add_thms inst thy = thy |> ProofContext.init - |> Proof.theorem_i Drule.internalK (K (fold add_thms)) NONE ("", []) + |> Proof.theorem_i Drule.internalK NONE (K (fold add_thms)) NONE ("", []) (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst)); in