src/HOL/Tools/recfun_codegen.ML
changeset 12556 5e2593ef0a44
parent 12447 e752c9aecdec
child 13105 3d1e7a199bdc
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Thu Dec 20 14:57:15 2001 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Thu Dec 20 14:57:54 2001 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  open Codegen;
     1.6  
     1.7 -structure RecfunArgs =
     1.8 +structure CodegenArgs =
     1.9  struct
    1.10    val name = "HOL/recfun_codegen";
    1.11    type T = thm list Symtab.table;
    1.12 @@ -28,7 +28,7 @@
    1.13    fun print _ _ = ();
    1.14  end;
    1.15  
    1.16 -structure RecfunData = TheoryDataFun(RecfunArgs);
    1.17 +structure CodegenData = TheoryDataFun(CodegenArgs);
    1.18  
    1.19  val prop_of = #prop o rep_thm;
    1.20  val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    1.21 @@ -40,19 +40,19 @@
    1.22  fun add (p as (thy, thm)) =
    1.23    let
    1.24      val tsig = Sign.tsig_of (sign_of thy);
    1.25 -    val tab = RecfunData.get thy;
    1.26 +    val tab = CodegenData.get thy;
    1.27      val (s, _) = const_of (prop_of thm);
    1.28  
    1.29      val matches = curry
    1.30        (Pattern.matches tsig o pairself (fst o dest_eqn o prop_of));
    1.31  
    1.32 -  in (RecfunData.put (Symtab.update ((s,
    1.33 +  in (CodegenData.put (Symtab.update ((s,
    1.34      filter_out (matches thm) (if_none (Symtab.lookup (tab, s)) []) @ [thm]),
    1.35        tab)) thy, thm)
    1.36    end handle TERM _ => (warn thm; p) | Pattern.Pattern => (warn thm; p);
    1.37  
    1.38  fun get_equations thy (s, T) =
    1.39 -  (case Symtab.lookup (RecfunData.get thy, s) of
    1.40 +  (case Symtab.lookup (CodegenData.get thy, s) of
    1.41       None => []
    1.42     | Some thms => filter (fn thm => is_instance thy T
    1.43         (snd (const_of (prop_of thm)))) thms);
    1.44 @@ -137,10 +137,8 @@
    1.45  
    1.46  
    1.47  val setup =
    1.48 -  [RecfunData.init,
    1.49 +  [CodegenData.init,
    1.50     add_codegen "recfun" recfun_codegen,
    1.51 -   Attrib.add_attributes [("code",
    1.52 -     (Attrib.no_args add, Attrib.no_args Attrib.undef_local_attribute),
    1.53 -     "declare equations to be used for code generation")]];
    1.54 +   add_attribute "" add];
    1.55  
    1.56  end;