--- 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;