src/HOL/Import/proof_kernel.ML
changeset 28677 4693938e9c2a
parent 28662 64ab5bb68d4c
child 28965 1de908189869
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Oct 23 15:28:08 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 23 15:28:39 2008 +0200
     1.3 @@ -1943,7 +1943,7 @@
     1.4          val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
     1.5          val rew = rewrite_hol4_term eq thy''
     1.6          val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
     1.7 -        val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
     1.8 +        val thy22 = if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn
     1.9                      then
    1.10                          let
    1.11                              val p1 = quotename constname
    1.12 @@ -2038,7 +2038,7 @@
    1.13              val th  = equal_elim rew res'
    1.14              fun handle_const (name,thy) =
    1.15                  let
    1.16 -                    val defname = def_name name
    1.17 +                    val defname = Thm.def_name name
    1.18                      val (newname,thy') = get_defname thyname name thy
    1.19                  in
    1.20                      (if defname = newname