TFL/thry.sml
changeset 3391 5e45dd3b64e9
parent 3388 dbf61e36f8e9
child 3405 2cccd0e3e9ea
     1.1 --- a/TFL/thry.sml	Tue Jun 03 10:56:04 1997 +0200
     1.2 +++ b/TFL/thry.sml	Tue Jun 03 11:08:08 1997 +0200
     1.3 @@ -55,14 +55,13 @@
     1.4   *---------------------------------------------------------------------------*)
     1.5  local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
     1.6        val Const(eeq_name, ty) = eeq
     1.7 -      val prop = #2 (S.strip_type ty)
     1.8 +      val prop = body_type ty
     1.9  in
    1.10  fun make_definition parent s tm = 
    1.11     let val {lhs,rhs} = S.dest_eq tm
    1.12 -       val (Name,Ty) = dest_Const lhs
    1.13 -       val lhs1 = S.mk_const{Name = Name, Ty = Ty}
    1.14 -       val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
    1.15 -       val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
    1.16 +       val (_,Ty) = dest_Const lhs
    1.17 +       val eeq1 = Const(eeq_name, Ty --> Ty --> prop)
    1.18 +       val dtm = list_comb(eeq1,[lhs,rhs])      (* Rename "=" to "==" *)
    1.19         val (_, tm', _) = Sign.infer_types (sign_of parent)
    1.20                       (K None) (K None) [] true ([dtm],propT)
    1.21         val new_thy = add_defs_i [(s,tm')] parent