Thm.get_def;
authorwenzelm
Thu Oct 23 16:07:03 2008 +0200 (2008-10-23)
changeset 28678d93980a6c3cb
parent 28677 4693938e9c2a
child 28679 d7384e8e99b3
Thm.get_def;
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Oct 23 15:28:39 2008 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Oct 23 16:07:03 2008 +0200
     1.3 @@ -303,7 +303,7 @@
     1.4  
     1.5    (*** Prove the recursor theorems ***)
     1.6  
     1.7 -  val recursor_eqns = case try (get_def thy1) recursor_base_name of
     1.8 +  val recursor_eqns = case try (Thm.get_def thy1) recursor_base_name of
     1.9       NONE => (writeln "  [ No recursion operator ]";
    1.10                [])
    1.11     | SOME recursor_def =>
     2.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Oct 23 15:28:39 2008 +0200
     2.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 23 16:07:03 2008 +0200
     2.3 @@ -182,7 +182,7 @@
     2.4  
     2.5    (*fetch fp definitions from the theory*)
     2.6    val big_rec_def::part_rec_defs =
     2.7 -    map (get_def thy1)
     2.8 +    map (Thm.get_def thy1)
     2.9          (case rec_names of [_] => rec_names
    2.10                           | _   => big_rec_base_name::rec_names);
    2.11