Sign.read_term;
authorwenzelm
Mon Aug 01 19:20:29 2005 +0200 (2005-08-01)
changeset 1697534ed8d5d4f16
parent 16974 0f8ebabf3163
child 16976 377962871f5d
Sign.read_term;
TFL/post.ML
src/HOL/Tools/inductive_package.ML
     1.1 --- a/TFL/post.ML	Mon Aug 01 19:20:28 2005 +0200
     1.2 +++ b/TFL/post.ML	Mon Aug 01 19:20:29 2005 +0200
     1.3 @@ -37,9 +37,6 @@
     1.4  
     1.5  (* misc *)
     1.6  
     1.7 -val read_term = Thm.term_of oo (HOLogic.read_cterm o Theory.sign_of);
     1.8 -
     1.9 -
    1.10  (*---------------------------------------------------------------------------
    1.11   * Extract termination goals so that they can be put it into a goalstack, or
    1.12   * have a tactic directly applied to them.
    1.13 @@ -248,7 +245,7 @@
    1.14    in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
    1.15  
    1.16  fun define strict thy cs ss congs wfs fid R seqs =
    1.17 -  define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
    1.18 +  define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs)
    1.19      handle U.ERR {mesg,...} => error mesg;
    1.20  
    1.21  
    1.22 @@ -275,7 +272,7 @@
    1.23   end
    1.24  
    1.25  fun defer thy congs fid seqs =
    1.26 -  defer_i thy congs fid (map (read_term thy) seqs)
    1.27 +  defer_i thy congs fid (map (Sign.read_term thy) seqs)
    1.28      handle U.ERR {mesg,...} => error mesg;
    1.29  end;
    1.30  
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Aug 01 19:20:28 2005 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Aug 01 19:20:29 2005 +0200
     2.3 @@ -614,7 +614,10 @@
     2.4        else
     2.5          (case ThyInfo.lookup_theory "Datatype" of
     2.6            NONE => []
     2.7 -        | SOME thy' => PureThy.get_thms thy' (Name "sum.cases")))
     2.8 +        | SOME thy' =>
     2.9 +            if Theory.subthy (thy', thy) then
    2.10 +              PureThy.get_thms thy' (Name "sum.cases")
    2.11 +            else []))
    2.12        |> map mk_meta_eq;
    2.13  
    2.14      val (preds, ind_prems, mutual_ind_concl, factors) =
    2.15 @@ -845,7 +848,7 @@
    2.16  
    2.17  fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
    2.18    let
    2.19 -    val cs = map (term_of o HOLogic.read_cterm thy) c_strings;
    2.20 +    val cs = map (Sign.read_term thy) c_strings;
    2.21  
    2.22      val intr_names = map (fst o fst) intro_srcs;
    2.23      fun read_rule s = Thm.read_cterm thy (s, propT)