src/Pure/Proof/extraction.ML
changeset 22846 fb79144af9a3
parent 22796 34c316d7b630
child 22924 17f1d7af43bd
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -171,11 +171,10 @@
     1.4  
     1.5  (**** theory data ****)
     1.6  
     1.7 -(* data kind 'Pure/extraction' *)
     1.8 +(* theory data *)
     1.9  
    1.10  structure ExtractionData = TheoryDataFun
    1.11 -(struct
    1.12 -  val name = "Pure/extraction";
    1.13 +(
    1.14    type T =
    1.15      {realizes_eqns : rules,
    1.16       typeof_eqns : rules,
    1.17 @@ -209,11 +208,7 @@
    1.18       defs = Library.merge Thm.eq_thm (defs1, defs2),
    1.19       expand = Library.merge (op =) (expand1, expand2),
    1.20       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    1.21 -
    1.22 -  fun print _ _ = ();
    1.23 -end);
    1.24 -
    1.25 -val _ = Context.add_setup ExtractionData.init;
    1.26 +);
    1.27  
    1.28  fun read_condeq thy =
    1.29    let val thy' = add_syntax thy