# HG changeset patch
# User berghofe
# Date 1008856674 -3600
# Node ID 5e2593ef0a4499a36274fa750d11227d17ecec22
# Parent  e6d7f040fdc72426ec0e1e93b337c8d58dabbb21
Moved "code" attribute to Pure/codegen.ML

diff -r e6d7f040fdc7 -r 5e2593ef0a44 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Thu Dec 20 14:57:15 2001 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Thu Dec 20 14:57:54 2001 +0100
@@ -17,7 +17,7 @@
 
 open Codegen;
 
-structure RecfunArgs =
+structure CodegenArgs =
 struct
   val name = "HOL/recfun_codegen";
   type T = thm list Symtab.table;
@@ -28,7 +28,7 @@
   fun print _ _ = ();
 end;
 
-structure RecfunData = TheoryDataFun(RecfunArgs);
+structure CodegenData = TheoryDataFun(CodegenArgs);
 
 val prop_of = #prop o rep_thm;
 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
@@ -40,19 +40,19 @@
 fun add (p as (thy, thm)) =
   let
     val tsig = Sign.tsig_of (sign_of thy);
-    val tab = RecfunData.get thy;
+    val tab = CodegenData.get thy;
     val (s, _) = const_of (prop_of thm);
 
     val matches = curry
       (Pattern.matches tsig o pairself (fst o dest_eqn o prop_of));
 
-  in (RecfunData.put (Symtab.update ((s,
+  in (CodegenData.put (Symtab.update ((s,
     filter_out (matches thm) (if_none (Symtab.lookup (tab, s)) []) @ [thm]),
       tab)) thy, thm)
   end handle TERM _ => (warn thm; p) | Pattern.Pattern => (warn thm; p);
 
 fun get_equations thy (s, T) =
-  (case Symtab.lookup (RecfunData.get thy, s) of
+  (case Symtab.lookup (CodegenData.get thy, s) of
      None => []
    | Some thms => filter (fn thm => is_instance thy T
        (snd (const_of (prop_of thm)))) thms);
@@ -137,10 +137,8 @@
 
 
 val setup =
-  [RecfunData.init,
+  [CodegenData.init,
    add_codegen "recfun" recfun_codegen,
-   Attrib.add_attributes [("code",
-     (Attrib.no_args add, Attrib.no_args Attrib.undef_local_attribute),
-     "declare equations to be used for code generation")]];
+   add_attribute "" add];
 
 end;