ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);
authorwenzelm
Tue Apr 03 19:24:10 2007 +0200 (2007-04-03)
changeset 22566535ae9dd4c45
parent 22565 2a1eef99bb6a
child 22567 1565d476a9e2
ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);
src/HOL/Tools/datatype_codegen.ML
src/Pure/Tools/codegen_data.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Apr 03 17:05:52 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Apr 03 19:24:10 2007 +0200
     1.3 @@ -623,7 +623,7 @@
     1.4          val const = ("op =", SOME dtco);
     1.5          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
     1.6        in
     1.7 -        CodegenData.add_funcl (const, CodegenData.lazy get_thms) thy
     1.8 +        CodegenData.add_funcl (const, CodegenData.lazy_thms get_thms) thy
     1.9        end;
    1.10    in
    1.11      prove_codetypes_arities (ClassPackage.intro_classes_tac [])
     2.1 --- a/src/Pure/Tools/codegen_data.ML	Tue Apr 03 17:05:52 2007 +0200
     2.2 +++ b/src/Pure/Tools/codegen_data.ML	Tue Apr 03 19:24:10 2007 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  
     2.5  signature CODEGEN_DATA =
     2.6  sig
     2.7 -  val lazy: (unit -> thm list) -> thm list Susp.T
     2.8 +  val lazy_thms: (unit -> thm list) -> thm list Susp.T
     2.9    val eval_always: bool ref
    2.10  
    2.11    val add_func: bool -> thm -> theory -> theory
    2.12 @@ -62,7 +62,7 @@
    2.13  
    2.14  val eval_always = ref false;
    2.15  
    2.16 -fun lazy f = if !eval_always
    2.17 +fun lazy_thms f = if !eval_always
    2.18    then Susp.value (f ())
    2.19    else Susp.delay f;
    2.20  
    2.21 @@ -79,7 +79,7 @@
    2.22     of SOME thms => (Susp.value o f thy) thms
    2.23       | NONE => let
    2.24            val thy_ref = Theory.self_ref thy;
    2.25 -        in lazy (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    2.26 +        in lazy_thms (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    2.27  
    2.28  fun merge' _ ([], []) = (false, [])
    2.29    | merge' _ ([], ys) = (true, ys)
    2.30 @@ -100,7 +100,7 @@
    2.31     of SOME [] => (true, r2)
    2.32      | _ => case Susp.peek r2
    2.33         of SOME [] => (true, r1)
    2.34 -        | _ => (apsnd (lazy o K)) (merge_thms (Susp.force r1, Susp.force r2));
    2.35 +        | _ => (apsnd (lazy_thms o K)) (merge_thms (Susp.force r1, Susp.force r2));
    2.36  
    2.37  
    2.38  
    2.39 @@ -128,7 +128,7 @@
    2.40    apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
    2.41  
    2.42  fun add_lthms lthms (sels, []) =
    2.43 -      (lazy (fn () => fold add_drop_redundant
    2.44 +      (lazy_thms (fn () => fold add_drop_redundant
    2.45          (Susp.force lthms) (Susp.force sels, []) |> fst), [])
    2.46          (*FIXME*)
    2.47    | add_lthms lthms (sels, dels) =
    2.48 @@ -146,7 +146,7 @@
    2.49      then let
    2.50        val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm dels1 (Susp.force sels2))
    2.51        val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm (Susp.force sels1) dels2)
    2.52 -    in (true, ((lazy o K) sels, dels)) end
    2.53 +    in (true, ((lazy_thms o K) sels, dels)) end
    2.54      else let
    2.55        val (sels_t, sels) = merge_lthms (sels1, sels2)
    2.56      in (sels_t, (sels, dels)) end