src/HOL/Tools/typecopy_package.ML
changeset 21675 38f6cb45ce24
parent 20855 9f60d493c8fe
child 21708 45e7491bea47
equal deleted inserted replaced
21674:8a6bf9d7c751 21675:38f6cb45ce24
    28   val setup: theory -> theory
    28   val setup: theory -> theory
    29 end;
    29 end;
    30 
    30 
    31 structure TypecopyPackage: TYPECOPY_PACKAGE =
    31 structure TypecopyPackage: TYPECOPY_PACKAGE =
    32 struct
    32 struct
    33 
       
    34 (* theory context reference *)
       
    35 
       
    36 val univ_witness = thm "Set.UNIV_witness"
       
    37 
       
    38 
    33 
    39 (* theory data *)
    34 (* theory data *)
    40 
    35 
    41 type info = {
    36 type info = {
    42   vs: (string * sort) list,
    37   vs: (string * sort) list,