# HG changeset patch
# User wenzelm
# Date 1305470424 -7200
# Node ID dda4aef7cba4c6ddb600a165c4277c62a23aa155
# Parent  c5146d5fc54c15df4cc4a256024b9d82edc5e3bc
tuned signature;

diff -r c5146d5fc54c -r dda4aef7cba4 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat May 14 22:00:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sun May 15 16:40:24 2011 +0200
@@ -798,7 +798,7 @@
 
 fun clasimpset_rules_of ctxt =
   let
-    val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
+    val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs
     val intros = Item_Net.content safeIs @ Item_Net.content hazIs
     val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
     val simps = ctxt |> simpset_of |> dest_ss |> #simps
diff -r c5146d5fc54c -r dda4aef7cba4 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat May 14 22:00:24 2011 +0200
+++ b/src/Provers/blast.ML	Sun May 15 16:40:24 2011 +0200
@@ -35,9 +35,6 @@
         "no DETERM" flag would prevent proofs failing here.
 *)
 
-(*Should be a type abbreviation?*)
-type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
-
 signature BLAST_DATA =
 sig
   structure Classical: CLASSICAL
@@ -554,7 +551,7 @@
   | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
 
 
-fun netMkRules ctxt P vars (nps: netpair list) =
+fun netMkRules ctxt P vars (nps: Classical.netpair list) =
   case P of
       (Const ("*Goal*", _) $ G) =>
         let val pG = mk_Trueprop (toTerm 2 G)
diff -r c5146d5fc54c -r dda4aef7cba4 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat May 14 22:00:24 2011 +0200
+++ b/src/Provers/classical.ML	Sun May 15 16:40:24 2011 +0200
@@ -18,11 +18,6 @@
   addSbefore addSafter addbefore addafter
   addD2 addE2 addSD2 addSE2;
 
-
-(*should be a type abbreviation in signature CLASSICAL*)
-type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
-type wrapper = (int -> tactic) -> (int -> tactic);
-
 signature CLASSICAL_DATA =
 sig
   val imp_elim: thm  (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
@@ -35,21 +30,8 @@
 
 signature BASIC_CLASSICAL =
 sig
+  type wrapper = (int -> tactic) -> int -> tactic
   type claset
-  val empty_cs: claset
-  val merge_cs: claset * claset -> claset
-  val rep_cs: claset ->
-   {safeIs: thm Item_Net.T,
-    safeEs: thm Item_Net.T,
-    hazIs: thm Item_Net.T,
-    hazEs: thm Item_Net.T,
-    swrappers: (string * (Proof.context -> wrapper)) list,
-    uwrappers: (string * (Proof.context -> wrapper)) list,
-    safe0_netpair: netpair,
-    safep_netpair: netpair,
-    haz_netpair: netpair,
-    dup_netpair: netpair,
-    xtra_netpair: Context_Rules.netpair}
   val print_claset: Proof.context -> unit
   val addDs: Proof.context * thm list -> Proof.context
   val addEs: Proof.context * thm list -> Proof.context
@@ -114,6 +96,19 @@
 sig
   include BASIC_CLASSICAL
   val classical_rule: thm -> thm
+  type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
+  val rep_cs: claset ->
+   {safeIs: thm Item_Net.T,
+    safeEs: thm Item_Net.T,
+    hazIs: thm Item_Net.T,
+    hazEs: thm Item_Net.T,
+    swrappers: (string * (Proof.context -> wrapper)) list,
+    uwrappers: (string * (Proof.context -> wrapper)) list,
+    safe0_netpair: netpair,
+    safep_netpair: netpair,
+    haz_netpair: netpair,
+    dup_netpair: netpair,
+    xtra_netpair: Context_Rules.netpair}
   val get_cs: Context.generic -> claset
   val map_cs: (claset -> claset) -> Context.generic -> Context.generic
   val safe_dest: int option -> attribute
@@ -213,6 +208,9 @@
 
 (**** Classical rule sets ****)
 
+type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
+type wrapper = (int -> tactic) -> int -> tactic;
+
 datatype claset =
   CS of
    {safeIs         : thm Item_Net.T,          (*safe introduction rules*)