# HG changeset patch
# User wenzelm
# Date 1393532878 -3600
# Node ID 687240115804c0cdc88d691ef3862986ff9768a0
# Parent  5821b1937fa5a6a6b0d4ffb398688a436e9e1aaf
tuned whitespace;
modernized theory setup;

diff -r 5821b1937fa5 -r 687240115804 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 27 21:02:09 2014 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 27 21:27:58 2014 +0100
@@ -12,8 +12,6 @@
 ML_file "langford_data.ML"
 ML_file "ferrante_rackoff_data.ML"
 
-setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *}
-
 context linorder
 begin
 
diff -r 5821b1937fa5 -r 687240115804 src/HOL/Decision_Procs/ferrante_rackoff_data.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Thu Feb 27 21:02:09 2014 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Thu Feb 27 21:27:58 2014 +0100
@@ -17,7 +17,6 @@
      whatis: morphism -> cterm -> cterm -> ord,
      simpset: morphism -> simpset} -> declaration
   val match: Proof.context -> cterm -> entry option
-  val setup: theory -> theory
 end;
 
 structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = 
@@ -117,28 +116,24 @@
 val terms = thms >> map Drule.dest_term;
 in
 
-val ferrak_setup =
-  Attrib.setup @{binding ferrack}
-    ((keyword minfN |-- thms)
-     -- (keyword pinfN |-- thms)
-     -- (keyword nmiN |-- thms)
-     -- (keyword npiN |-- thms)
-     -- (keyword lin_denseN |-- thms)
-     -- (keyword qeN |-- thms)
-     -- (keyword atomsN |-- terms) >>
-       (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
-       if length qe = 1 then
-         add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
-              qe = hd qe, atoms = atoms},
-             {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
-       else error "only one theorem for qe!"))
-    "Ferrante Rackoff data";
+val _ =
+  Theory.setup
+    (Attrib.setup @{binding ferrack}
+      ((keyword minfN |-- thms)
+       -- (keyword pinfN |-- thms)
+       -- (keyword nmiN |-- thms)
+       -- (keyword npiN |-- thms)
+       -- (keyword lin_denseN |-- thms)
+       -- (keyword qeN |-- thms)
+       -- (keyword atomsN |-- terms) >>
+         (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
+         if length qe = 1 then
+           add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
+                qe = hd qe, atoms = atoms},
+               {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
+         else error "only one theorem for qe!"))
+      "Ferrante Rackoff data");
 
 end;
 
-
-(* theory setup *)
-
-val setup = ferrak_setup;
-
 end;
diff -r 5821b1937fa5 -r 687240115804 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Thu Feb 27 21:02:09 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Feb 27 21:27:58 2014 +0100
@@ -12,19 +12,20 @@
 struct
 
 val dest_set =
- let
-  fun h acc ct =
-   case term_of ct of
-     Const (@{const_name Orderings.bot}, _) => acc
-   | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
-in h [] end;
+  let
+    fun h acc ct =
+      (case term_of ct of
+        Const (@{const_name Orderings.bot}, _) => acc
+      | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct));
+  in h [] end;
 
 fun prove_finite cT u =
-let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
+  let
+    val [th0, th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
     fun ins x th =
-     Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
-                                     (Thm.cprop_of th), SOME x] th1) th
-in fold ins u th0 end;
+      Thm.implies_elim
+        (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
+  in fold ins u th0 end;
 
 fun simp_rule ctxt =
   Conv.fconv_rule
diff -r 5821b1937fa5 -r 687240115804 src/HOL/Decision_Procs/langford_data.ML
--- a/src/HOL/Decision_Procs/langford_data.ML	Thu Feb 27 21:02:09 2014 +0100
+++ b/src/HOL/Decision_Procs/langford_data.ML	Thu Feb 27 21:27:58 2014 +0100
@@ -2,18 +2,20 @@
 sig
   type entry
   val get: Proof.context -> simpset * (thm * entry) list
-  val add: entry -> attribute 
+  val add: entry -> attribute
   val del: attribute
-  val setup: theory -> theory
   val match: Proof.context -> cterm -> entry option
 end;
 
-structure Langford_Data: LANGFORD_DATA = 
+structure Langford_Data: LANGFORD_DATA =
 struct
 
 (* data *)
-type entry = {qe_bnds: thm, qe_nolb : thm , qe_noub: thm, 
-              gs : thm list, gst : thm, atoms: cterm list};
+
+type entry =
+  {qe_bnds: thm, qe_nolb : thm , qe_noub: thm,
+   gs : thm list, gst : thm, atoms: cterm list};
+
 val eq_key = Thm.eq_thm;
 fun eq_data arg = eq_fst eq_key arg;
 
@@ -32,9 +34,9 @@
 
 val del = Thm.declaration_attribute (Data.map o del_data);
 
-fun add entry = 
-    Thm.declaration_attribute (fn key => fn context => context |> Data.map 
-      (del_data key #> apsnd (cons (key, entry))));
+fun add entry =
+  Thm.declaration_attribute (fn key => fn context => context |> Data.map
+    (del_data key #> apsnd (cons (key, entry))));
 
 val add_simp = Thm.declaration_attribute (fn th => fn context =>
   (Data.map o apfst) (simpset_map (Context.proof_of context) (Simplifier.add_simp th)) context);
@@ -44,70 +46,68 @@
 
 fun match ctxt tm =
   let
-    fun match_inst
-        {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat =
-       let
+    fun match_inst {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat =
+      let
         fun h instT =
           let
             val substT = Thm.instantiate (instT, []);
             val substT_cterm = Drule.cterm_rule substT;
 
-            val qe_bnds' = substT qe_bnds
-            val qe_nolb' = substT qe_nolb
-            val qe_noub' = substT qe_noub
-            val gs' = map substT gs
-            val gst' = substT gst
-            val atoms' = map substT_cterm atoms
-            val result = {qe_bnds = qe_bnds', qe_nolb = qe_nolb', 
-                          qe_noub = qe_noub', gs = gs', gst = gst', 
-                          atoms = atoms'}
-          in SOME result end
-      in (case try Thm.match (pat, tm) of
-           NONE => NONE
-         | SOME (instT, _) => h instT)
+            val qe_bnds' = substT qe_bnds;
+            val qe_nolb' = substT qe_nolb;
+            val qe_noub' = substT qe_noub;
+            val gs' = map substT gs;
+            val gst' = substT gst;
+            val atoms' = map substT_cterm atoms;
+            val result =
+             {qe_bnds = qe_bnds', qe_nolb = qe_nolb',
+              qe_noub = qe_noub', gs = gs', gst = gst',
+              atoms = atoms'};
+          in SOME result end;
+      in
+        (case try Thm.match (pat, tm) of
+          NONE => NONE
+        | SOME (instT, _) => h instT)
       end;
 
-    fun match_struct (_,
-        entry as ({atoms = atoms, ...}): entry) =
+    fun match_struct (_, entry as ({atoms = atoms, ...}): entry) =
       get_first (match_inst entry) atoms;
   in get_first match_struct (snd (get ctxt)) end;
 
+
 (* concrete syntax *)
 
 local
-val qeN = "qe";
-val gatherN = "gather";
-val atomsN = "atoms"
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-val any_keyword =
-  keyword qeN || keyword gatherN || keyword atomsN;
+  val qeN = "qe";
+  val gatherN = "gather";
+  val atomsN = "atoms"
+  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+  val any_keyword = keyword qeN || keyword gatherN || keyword atomsN;
 
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-val terms = thms >> map Drule.dest_term;
+  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+  val terms = thms >> map Drule.dest_term;
 in
 
-val langford_setup =
-  Attrib.setup @{binding langford}
-    ((keyword qeN |-- thms)
-     -- (keyword gatherN |-- thms)
-     -- (keyword atomsN |-- terms) >>
-       (fn ((qes,gs), atoms) => 
-       if length qes = 3 andalso length gs > 1 then
-         let 
-           val [q1,q2,q3] = qes
-           val gst::gss = gs
-           val entry = {qe_bnds = q1, qe_nolb = q2,
-                        qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
-         in add entry end
-       else error "Need 3 theorems for qe and at least one for gs"))
-    "Langford data";
+val _ =
+  Theory.setup
+    (Attrib.setup @{binding langford}
+      ((keyword qeN |-- thms) --
+       (keyword gatherN |-- thms) --
+       (keyword atomsN |-- terms) >> (fn ((qes, gs), atoms) =>
+          if length qes = 3 andalso length gs > 1 then
+            let
+              val [q1, q2, q3] = qes;
+              val gst :: gss = gs;
+              val entry =
+               {qe_bnds = q1, qe_nolb = q2,
+                qe_noub = q3, gs = gss, gst = gst, atoms = atoms};
+            in add entry end
+          else error "Need 3 theorems for qe and at least one for gs"))
+      "Langford data");
+end;
+
+val _ =
+  Theory.setup
+    (Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset");
 
 end;
-
-(* theory setup *)
-
-val setup =
-  langford_setup #>
-  Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
-
-end;