src/HOL/Import/proof_kernel.ML
changeset 29270 0eade173f77e
parent 29265 5b4247055bd7
child 29281 b22ccb3998db
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Dec 31 15:30:10 2008 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 31 18:53:16 2008 +0100
     1.3 @@ -1149,7 +1149,7 @@
     1.4        val t = term_of ct
     1.5        val thy = theory_of_cterm ct
     1.6        val frees = OldTerm.term_frees t
     1.7 -      val freenames = add_term_free_names (t, [])
     1.8 +      val freenames = OldTerm.add_term_free_names (t, [])
     1.9        fun is_old_name n = n mem_string freenames
    1.10        fun name_of (Free (n, _)) = n
    1.11          | name_of _ = ERR "name_of"
    1.12 @@ -1218,7 +1218,7 @@
    1.13                           c = "All" orelse
    1.14                           c = "op -->" orelse
    1.15                           c = "op &" orelse
    1.16 -                         c = "op =")) (Term.term_consts tm)
    1.17 +                         c = "op =")) (OldTerm.term_consts tm)
    1.18  
    1.19  fun match_consts t (* th *) =
    1.20      let
    1.21 @@ -1423,9 +1423,9 @@
    1.22      let
    1.23          val _ = message "INST_TYPE:"
    1.24          val _ = if_debug pth hth
    1.25 -        val tys_before = add_term_tfrees (prop_of th,[])
    1.26 +        val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
    1.27          val th1 = Thm.varifyT th
    1.28 -        val tys_after = add_term_tvars (prop_of th1,[])
    1.29 +        val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
    1.30          val tyinst = map (fn (bef, iS) =>
    1.31                               (case try (Lib.assoc (TFree bef)) lambda of
    1.32                                    SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
    1.33 @@ -2092,7 +2092,7 @@
    1.34              val c = case concl_of th2 of
    1.35                          _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
    1.36                        | _ => raise ERR "new_type_definition" "Bad type definition theorem"
    1.37 -            val tfrees = term_tfrees c
    1.38 +            val tfrees = OldTerm.term_tfrees c
    1.39              val tnames = map fst tfrees
    1.40              val tsyn = mk_syn thy tycname
    1.41              val typ = (tycname,tnames,tsyn)
    1.42 @@ -2178,7 +2178,7 @@
    1.43              val c = case concl_of th2 of
    1.44                          _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
    1.45                        | _ => raise ERR "type_introduction" "Bad type definition theorem"
    1.46 -            val tfrees = term_tfrees c
    1.47 +            val tfrees = OldTerm.term_tfrees c
    1.48              val tnames = sort string_ord (map fst tfrees)
    1.49              val tsyn = mk_syn thy tycname
    1.50              val typ = (tycname,tnames,tsyn)