src/HOL/Tools/datatype_package.ML
changeset 19539 5b37bb0ad964
parent 19346 c4c003abd830
child 19599 a5c7eb37d14f
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue May 02 20:42:34 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue May 02 20:42:35 2006 +0200
     1.3 @@ -356,28 +356,28 @@
     1.4  
     1.5  exception ConstrDistinct of term;
     1.6  
     1.7 -fun distinct_proc sg ss (t as Const ("op =", _) $ t1 $ t2) =
     1.8 +fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
     1.9    (case (stripC (0, t1), stripC (0, t2)) of
    1.10       ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
    1.11           (case (stripT (0, T1), stripT (0, T2)) of
    1.12              ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
    1.13                  if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
    1.14 -                   (case (get_datatype_descr sg) tname1 of
    1.15 +                   (case (get_datatype_descr thy) tname1 of
    1.16                        SOME (_, (_, constrs)) => let val cnames = map fst constrs
    1.17                          in if cname1 mem cnames andalso cname2 mem cnames then
    1.18                               let val eq_t = Logic.mk_equals (t, Const ("False", HOLogic.boolT));
    1.19 -                                 val eq_ct = cterm_of sg eq_t;
    1.20 -                                 val Datatype_thy = theory "Datatype";
    1.21 +                                 val eq_ct = cterm_of thy eq_t;
    1.22 +                                 val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
    1.23                                   val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
    1.24                                     map (get_thm Datatype_thy o Name)
    1.25                                       ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
    1.26 -                             in (case (#distinct (the_datatype sg tname1)) of
    1.27 +                             in (case (#distinct (the_datatype thy tname1)) of
    1.28                                   QuickAndDirty => SOME (Thm.invoke_oracle
    1.29 -                                   Datatype_thy distinctN (sg, ConstrDistinct eq_t))
    1.30 -                               | FewConstrs thms => SOME (Goal.prove sg [] [] eq_t (K
    1.31 +                                   Datatype_thy distinctN (thy, ConstrDistinct eq_t))
    1.32 +                               | FewConstrs thms => SOME (Goal.prove thy [] [] eq_t (K
    1.33                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.34                                      atac 2, resolve_tac thms 1, etac FalseE 1])))
    1.35 -                               | ManyConstrs (thm, simpset) => SOME (Goal.prove sg [] [] eq_t (K
    1.36 +                               | ManyConstrs (thm, simpset) => SOME (Goal.prove thy [] [] eq_t (K
    1.37                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.38                                      full_simp_tac (Simplifier.inherit_context ss simpset) 1,
    1.39                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.40 @@ -390,7 +390,7 @@
    1.41                  else NONE
    1.42            | _ => NONE)
    1.43     | _ => NONE)
    1.44 -  | distinct_proc sg _ _ = NONE;
    1.45 +  | distinct_proc thy _ _ = NONE;
    1.46  
    1.47  val distinct_simproc =
    1.48    Simplifier.simproc HOL.thy distinctN ["s = t"] distinct_proc;