# HG changeset patch
# User wenzelm
# Date 1458586676 -3600
# Node ID 646b84666a567b66642fd3261ebee058974f7f20
# Parent  092cb9c96c99a9b9f4bd7eb61b32192d9f155b2a
eliminated unused argument (see also 58110c1e02bc);

diff -r 092cb9c96c99 -r 646b84666a56 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Mar 21 11:54:45 2016 +0100
+++ b/src/Pure/Isar/element.ML	Mon Mar 21 19:57:56 2016 +0100
@@ -40,10 +40,9 @@
   val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) ->
     term list list -> term list -> Proof.context -> Proof.state
   val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
-    string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
+    string -> term list list -> Proof.context -> Proof.state -> Proof.state
   val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
-    string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
-    Proof.state
+    string -> term list list -> term list -> Proof.context -> Proof.state -> Proof.state
   val transform_witness: morphism -> witness -> witness
   val conclude_witness: Proof.context -> witness -> thm
   val pretty_witness: Proof.context -> witness -> Pretty.T
@@ -285,7 +284,7 @@
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness end;
 
-fun proof_local cmd goal_ctxt int after_qed propp =
+fun proof_local cmd goal_ctxt after_qed propp =
   let
     fun after_qed' (result_ctxt, results) state' =
       after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state';
@@ -303,12 +302,12 @@
 
 val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
 
-fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
-  gen_witness_proof (proof_local cmd goal_ctxt int)
+fun witness_local_proof after_qed cmd wit_propss goal_ctxt =
+  gen_witness_proof (proof_local cmd goal_ctxt)
     (fn wits => fn _ => after_qed wits) wit_propss [];
 
-fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
-  gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
+fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt =
+  gen_witness_proof (proof_local cmd goal_ctxt) after_qed wit_propss eq_props;
 
 end;
 
diff -r 092cb9c96c99 -r 646b84666a56 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Mon Mar 21 11:54:45 2016 +0100
+++ b/src/Pure/Isar/interpretation.ML	Mon Mar 21 19:57:56 2016 +0100
@@ -11,10 +11,8 @@
   type 'a rewrites = (Attrib.binding * 'a) list
 
   (*interpretation in proofs*)
-  val interpret: Expression.expression_i ->
-    term rewrites -> bool -> Proof.state -> Proof.state
-  val interpret_cmd: Expression.expression ->
-    string rewrites -> bool -> Proof.state -> Proof.state
+  val interpret: Expression.expression_i -> term rewrites -> Proof.state -> Proof.state
+  val interpret_cmd: Expression.expression -> string rewrites -> Proof.state -> Proof.state
 
   (*interpretation in local theories*)
   val interpretation: Expression.expression_i ->
@@ -160,7 +158,7 @@
 
 local
 
-fun gen_interpret prep_interpretation expression raw_eqns int state =
+fun gen_interpret prep_interpretation expression raw_eqns state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
@@ -168,7 +166,7 @@
       Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
     fun setup_proof after_qed propss eqns goal_ctxt =
       Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
-        propss eqns goal_ctxt int state;
+        propss eqns goal_ctxt state;
   in
     generic_interpretation prep_interpretation setup_proof
       Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
diff -r 092cb9c96c99 -r 646b84666a56 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Mar 21 11:54:45 2016 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 21 19:57:56 2016 +0100
@@ -396,7 +396,7 @@
   Outer_Syntax.command @{command_keyword interpret}
     "prove interpretation of locale expression in proof context"
     (interpretation_args >> (fn (expr, equations) =>
-      Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
+      Toplevel.proof (Interpretation.interpret_cmd expr equations)));
 
 val interpretation_args_with_defs =
   Parse.!!! Parse_Spec.locale_expression --