src/HOL/Tools/datatype_aux.ML
changeset 6394 3d9fd50fcc43
parent 6092 d9db67970c73
child 7015 85be09eb136c
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Wed Mar 17 16:53:32 1999 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Wed Mar 17 16:53:46 1999 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  fun foldl1 f (x::xs) = foldl f (x, xs);
     1.5  
     1.6  fun get_thy name thy = find_first
     1.7 -  (equal name o Sign.name_of o sign_of) (ancestors_of thy);
     1.8 +  (equal name o Sign.name_of o Theory.sign_of) (Theory.ancestors_of thy);
     1.9  
    1.10  fun add_path flat_names s = if flat_names then I else Theory.add_path s;
    1.11  fun parent_path flat_names = if flat_names then I else Theory.parent_path;
    1.12 @@ -113,7 +113,7 @@
    1.13          None => let val [Free (s, T)] = add_term_frees (t2, [])
    1.14            in absfree (s, T, t2) end
    1.15        | Some (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
    1.16 -    val cert = cterm_of (sign_of_thm st);
    1.17 +    val cert = cterm_of (Thm.sign_of_thm st);
    1.18      val Ps = map (cert o head_of o snd o getP) ts;
    1.19      val indrule' = cterm_instantiate (Ps ~~
    1.20        (map (cert o abstr o getP) ts')) indrule
    1.21 @@ -125,7 +125,7 @@
    1.22  
    1.23  fun exh_tac exh_thm_of i state =
    1.24    let
    1.25 -    val sg = sign_of_thm state;
    1.26 +    val sg = Thm.sign_of_thm state;
    1.27      val prem = nth_elem (i - 1, prems_of state);
    1.28      val params = Logic.strip_params prem;
    1.29      val (_, Type (tname, _)) = hd (rev params);