--- a/src/Pure/Isar/isar_syn.ML Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Apr 10 21:31:05 2012 +0200
@@ -464,7 +464,7 @@
(Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
val _ =
- Outer_Syntax.command ("sublocale", Keyword.thy_goal)
+ Outer_Syntax.command ("sublocale", Keyword.thy_schematic_goal)
"prove sublocale relation between a locale and a locale expression"
(Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
parse_interpretation_arguments false
@@ -472,7 +472,7 @@
Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
val _ =
- Outer_Syntax.command ("interpretation", Keyword.thy_goal)
+ Outer_Syntax.command ("interpretation", Keyword.thy_schematic_goal)
"prove interpretation of locale expression in theory"
(parse_interpretation_arguments true
>> (fn (expr, equations) => Toplevel.print o
--- a/src/Pure/Isar/outer_syntax.ML Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Tue Apr 10 21:31:05 2012 +0200
@@ -296,7 +296,8 @@
val (tr, proper_head) = read head |>> Toplevel.modify_init init;
val proof_trs = map read proof |> filter #2 |> map #1;
in
- if proper_head andalso proper_proof then [(tr, proof_trs)]
+ if proper_head andalso proper_proof andalso
+ not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
end;
--- a/src/Pure/Isar/proof.ML Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/proof.ML Tue Apr 10 21:31:05 2012 +0200
@@ -112,11 +112,8 @@
val show_cmd: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val schematic_goal: state -> bool
- val is_relevant: state -> bool
- val local_future_proof: (state -> ('a * state) Future.future) ->
- state -> 'a Future.future * state
- val global_future_proof: (state -> ('a * Proof.context) Future.future) ->
- state -> 'a Future.future * context
+ val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
+ val global_future_proof: (state -> ('a * Proof.context) future) -> state -> 'a future * context
val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
end;
--- a/src/Pure/Isar/toplevel.ML Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Apr 10 21:31:05 2012 +0200
@@ -672,12 +672,7 @@
fun proof_result immediate (tr, proof_trs) st =
let val st' = command tr st in
- if immediate orelse
- null proof_trs orelse
- Keyword.is_schematic_goal (name_of tr) orelse
- exists (Keyword.is_qed_global o name_of) proof_trs orelse
- not (can proof_of st') orelse
- Proof.is_relevant (proof_of st')
+ if immediate orelse null proof_trs orelse not (can proof_of st')
then
let val (states, st'') = fold_map command_result proof_trs st'
in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end