# HG changeset patch
# User wenzelm
# Date 1248463305 -7200
# Node ID 893614e2c35c3d33f09e72fd6a7ef628368795db
# Parent  a89979440d2c6fd37595958877125badee65dcc6
renamed functor BlastFun to Blast, require explicit theory;
eliminated src/FOL/blastdata.ML;

diff -r a89979440d2c -r 893614e2c35c src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Jul 24 21:18:05 2009 +0200
+++ b/src/FOL/FOL.thy	Fri Jul 24 21:21:45 2009 +0200
@@ -12,7 +12,6 @@
   "~~/src/Provers/clasimp.ML"
   "~~/src/Tools/induct.ML"
   ("cladata.ML")
-  ("blastdata.ML")
   ("simpdata.ML")
 begin
 
@@ -171,7 +170,25 @@
 setup Cla.setup
 setup cla_setup
 
-use "blastdata.ML"
+ML {*
+  structure Blast = Blast
+  (
+    val thy = @{theory}
+    type claset	= Cla.claset
+    val equality_name = @{const_name "op ="}
+    val not_name = @{const_name Not}
+    val notE	= @{thm notE}
+    val ccontr	= @{thm ccontr}
+    val contr_tac = Cla.contr_tac
+    val dup_intr	= Cla.dup_intr
+    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
+    val rep_cs = Cla.rep_cs
+    val cla_modifiers = Cla.cla_modifiers
+    val cla_meth' = Cla.cla_meth'
+  );
+  val blast_tac = Blast.blast_tac;
+*}
+
 setup Blast.setup
 
 
diff -r a89979440d2c -r 893614e2c35c src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Fri Jul 24 21:18:05 2009 +0200
+++ b/src/FOL/IsaMakefile	Fri Jul 24 21:21:45 2009 +0200
@@ -36,8 +36,8 @@
   $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
   $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
   $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
-  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML	\
-  cladata.ML document/root.tex fologic.ML hypsubstdata.ML intprover.ML	\
+  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML cladata.ML	\
+  document/root.tex fologic.ML hypsubstdata.ML intprover.ML		\
   simpdata.ML
 	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
 
diff -r a89979440d2c -r 893614e2c35c src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Fri Jul 24 21:18:05 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-
-(*** Applying BlastFun to create blast_tac ***)
-structure Blast_Data = 
-  struct
-  type claset	= Cla.claset
-  val equality_name = @{const_name "op ="}
-  val not_name = @{const_name Not}
-  val notE	= @{thm notE}
-  val ccontr	= @{thm ccontr}
-  val contr_tac = Cla.contr_tac
-  val dup_intr	= Cla.dup_intr
-  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
-  val rep_cs = Cla.rep_cs
-  val cla_modifiers = Cla.cla_modifiers;
-  val cla_meth' = Cla.cla_meth'
-  end;
-
-structure Blast = BlastFun(Blast_Data);
-val blast_tac = Blast.blast_tac;
diff -r a89979440d2c -r 893614e2c35c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jul 24 21:18:05 2009 +0200
+++ b/src/HOL/HOL.thy	Fri Jul 24 21:21:45 2009 +0200
@@ -910,8 +910,9 @@
 done
 
 ML {*
-structure Blast = BlastFun
+structure Blast = Blast
 (
+  val thy = @{theory}
   type claset = Classical.claset
   val equality_name = @{const_name "op ="}
   val not_name = @{const_name Not}
diff -r a89979440d2c -r 893614e2c35c src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Jul 24 21:18:05 2009 +0200
+++ b/src/Provers/blast.ML	Fri Jul 24 21:21:45 2009 +0200
@@ -39,7 +39,8 @@
 type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
 
 signature BLAST_DATA =
-  sig
+sig
+  val thy: theory
   type claset
   val equality_name: string
   val not_name: string
@@ -57,11 +58,10 @@
                  haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
   val cla_modifiers: Method.modifier parser list
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
-  end;
-
+end;
 
 signature BLAST =
-  sig
+sig
   type claset
   exception TRANS of string    (*reports translation errors*)
   datatype term =
@@ -90,10 +90,10 @@
   val tryInThy          : theory -> claset -> int -> string ->
                   (int->tactic) list * branch list list * (int*int*exn) list
   val normBr            : branch -> branch
-  end;
+end;
 
 
-functor BlastFun(Data: BLAST_DATA) : BLAST =
+functor Blast(Data: BLAST_DATA) : BLAST =
 struct
 
 type claset = Data.claset;
@@ -181,8 +181,8 @@
 fun isGoal (Const ("*Goal*", _) $ _) = true
   | isGoal _ = false;
 
-val TruepropC = ObjectLogic.judgment_name (OldGoals.the_context ());
-val TruepropT = Sign.the_const_type (OldGoals.the_context ()) TruepropC;
+val TruepropC = ObjectLogic.judgment_name Data.thy;
+val TruepropT = Sign.the_const_type Data.thy TruepropC;
 
 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);