src/HOL/Import/proof_kernel.ML
changeset 35994 9cc3df9a606e
parent 35845 e5980f0ad025
child 36543 0e7fc5bf38de
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Mar 27 18:43:11 2010 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 27 21:38:38 2010 +0100
     1.3 @@ -2098,7 +2098,7 @@
     1.4                  (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy
     1.5              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
     1.6  
     1.7 -            val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
     1.8 +            val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4
     1.9  
    1.10              val fulltyname = Sign.intern_type thy' tycname
    1.11              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
    1.12 @@ -2195,7 +2195,7 @@
    1.13                      [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
    1.14                      [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
    1.15                      typedef_hol2hollight
    1.16 -            val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
    1.17 +            val th4 = (#type_definition (#2 typedef_info)) RS typedef_hol2hollight'
    1.18              val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse
    1.19                raise ERR "type_introduction" "no type variables expected any more"
    1.20              val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse