TFL/thry.sml
changeset 3245 241838c01caf
parent 3191 14bd6e5985f1
child 3302 404fe31fd8d2
     1.1 --- a/TFL/thry.sml	Tue May 20 11:47:33 1997 +0200
     1.2 +++ b/TFL/thry.sml	Tue May 20 11:49:57 1997 +0200
     1.3 @@ -2,11 +2,6 @@
     1.4  struct
     1.5  
     1.6  structure USyntax  = USyntax;
     1.7 -type Type = USyntax.Type
     1.8 -type Preterm = USyntax.Preterm
     1.9 -type Term = USyntax.Term
    1.10 -type Thm = Thm.thm
    1.11 -type Thry = theory;
    1.12  
    1.13  open Mask;
    1.14  structure S = USyntax;
    1.15 @@ -66,9 +61,9 @@
    1.16         val {Name,Ty} = S.dest_var lhs
    1.17         val lhs1 = S.mk_const{Name = Name, Ty = Ty}
    1.18         val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
    1.19 -       val dtm = S.list_mk_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
    1.20 +       val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
    1.21         val (_, tm', _) = Sign.infer_types (sign_of parent)
    1.22 -	             (K None) (K None) [] true ([dtm],propT)
    1.23 +                     (K None) (K None) [] true ([dtm],propT)
    1.24         val new_thy = add_defs_i [(s,tm')] parent
    1.25     in 
    1.26     (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
    1.27 @@ -112,24 +107,24 @@
    1.28   * is temporary, I hope!
    1.29   *---------------------------------------------------------------------------*)
    1.30  val match_info = fn thy =>
    1.31 -    fn "*" => Utils.SOME({case_const = #case_const (#2 prod_record),
    1.32 +    fn "*" => Some({case_const = #case_const (#2 prod_record),
    1.33                       constructors = #constructors (#2 prod_record)})
    1.34 -     | "nat" => Utils.SOME({case_const = #case_const (#2 nat_record),
    1.35 +     | "nat" => Some({case_const = #case_const (#2 nat_record),
    1.36                         constructors = #constructors (#2 nat_record)})
    1.37       | ty => case assoc(!datatypes,ty)
    1.38 -               of None => Utils.NONE
    1.39 +               of None => None
    1.40                  | Some{case_const,constructors, ...} =>
    1.41 -                   Utils.SOME{case_const=case_const, constructors=constructors}
    1.42 +                   Some{case_const=case_const, constructors=constructors}
    1.43  
    1.44  val induct_info = fn thy =>
    1.45 -    fn "*" => Utils.SOME({nchotomy = #nchotomy (#2 prod_record),
    1.46 +    fn "*" => Some({nchotomy = #nchotomy (#2 prod_record),
    1.47                       constructors = #constructors (#2 prod_record)})
    1.48 -     | "nat" => Utils.SOME({nchotomy = #nchotomy (#2 nat_record),
    1.49 +     | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
    1.50                         constructors = #constructors (#2 nat_record)})
    1.51       | ty => case assoc(!datatypes,ty)
    1.52 -               of None => Utils.NONE
    1.53 +               of None => None
    1.54                  | Some{nchotomy,constructors, ...} =>
    1.55 -                  Utils.SOME{nchotomy=nchotomy, constructors=constructors}
    1.56 +                  Some{nchotomy=nchotomy, constructors=constructors}
    1.57  
    1.58  val extract_info = fn thy => 
    1.59   let val case_congs = map (#case_cong o #2) (!datatypes)
    1.60 @@ -140,5 +135,4 @@
    1.61                       #case_rewrites(#2 nat_record)@case_rewrites}
    1.62   end;
    1.63  
    1.64 -
    1.65  end; (* Thry *)