src/HOL/Import/proof_kernel.ML
changeset 29585 c23295521af5
parent 29289 f45c9c3b40a3
child 30190 479806475f3c
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Jan 21 16:51:45 2009 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Jan 21 18:27:43 2009 +0100
     1.3 @@ -1928,7 +1928,7 @@
     1.4                         Replaying _ => thy
     1.5                       | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
     1.6          val eq = mk_defeq constname rhs' thy1
     1.7 -        val (thms, thy2) = PureThy.add_defs false [((thmname,eq),[])] thy1
     1.8 +        val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1
     1.9          val _ = ImportRecorder.add_defs thmname eq
    1.10          val def_thm = hd thms
    1.11          val thm' = def_thm RS meta_eq_to_obj_eq_thm