src/HOL/Tools/SMT2/z3_new_replay_methods.ML
changeset 57220 853557cf2efa
parent 57145 7292a7258750
child 57229 489083abce44
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Wed Jun 11 19:15:54 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Wed Jun 11 19:15:55 2014 +0200
@@ -49,7 +49,6 @@
   val nnf_neg: z3_method
   val mp_oeq: z3_method
   val th_lemma: string -> z3_method
-  val is_assumption: Z3_New_Proof.z3_rule -> bool
   val method_for: Z3_New_Proof.z3_rule -> z3_method
 end
 
@@ -646,13 +645,6 @@
 
 (* mapping of rules to methods *)
 
-fun is_assumption Z3_New_Proof.Asserted = true
-  | is_assumption Z3_New_Proof.Goal = true
-  | is_assumption Z3_New_Proof.Hypothesis = true
-  | is_assumption Z3_New_Proof.Intro_Def = true
-  | is_assumption Z3_New_Proof.Skolemize = true
-  | is_assumption _ = false
-
 fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
 fun assumed rule ctxt = replay_error ctxt "Assumed" rule