src/FOLP/simp.ML
changeset 22578 b0eb5652f210
parent 22360 26ead7ed4f4b
child 22596 d0d2af4db18f
     1.1 --- a/src/FOLP/simp.ML	Wed Apr 04 00:10:59 2007 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Apr 04 00:11:03 2007 +0200
     1.3 @@ -359,13 +359,7 @@
     1.4  
     1.5  datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE
     1.6                 | PROVE | POP_CS | POP_ARTR | IF;
     1.7 -(*
     1.8 -fun pr_cntrl c = case c of STOP => std_output("STOP") | MK_EQ => std_output("MK_EQ") |
     1.9 -ASMS i => print_int i | POP_ARTR => std_output("POP_ARTR") |
    1.10 -SIMP_LHS => std_output("SIMP_LHS") | REW => std_output("REW") | REFL => std_output("REFL") |
    1.11 -TRUE => std_output("TRUE") | PROVE => std_output("PROVE") | POP_CS => std_output("POP_CS") | IF
    1.12 -=> std_output("IF");
    1.13 -*)
    1.14 +
    1.15  fun simp_refl([],_,ss) = ss
    1.16    | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss)
    1.17          else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss);
    1.18 @@ -589,23 +583,21 @@
    1.19  end;
    1.20  
    1.21  fun mk_cong_thy thy f =
    1.22 -let val sg = sign_of thy;
    1.23 -    val T = case Sign.const_type sg f of
    1.24 +let val T = case Sign.const_type thy f of
    1.25                  NONE => error(f^" not declared") | SOME(T) => T;
    1.26      val T' = Logic.incr_tvar 9 T;
    1.27 -in mk_cong_type sg (Const(f,T'),T') end;
    1.28 +in mk_cong_type thy (Const(f,T'),T') end;
    1.29  
    1.30  fun mk_congs thy = List.concat o map (mk_cong_thy thy);
    1.31  
    1.32  fun mk_typed_congs thy =
    1.33 -let val sg = sign_of thy;
    1.34 -    val S0 = Sign.defaultS sg;
    1.35 +let val S0 = Sign.defaultS thy;
    1.36      fun readfT(f,s) =
    1.37 -        let val T = Logic.incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
    1.38 -            val t = case Sign.const_type sg f of
    1.39 +        let val T = Logic.incr_tvar 9 (Sign.read_typ(thy, K(SOME(S0))) s);
    1.40 +            val t = case Sign.const_type thy f of
    1.41                        SOME(_) => Const(f,T) | NONE => Free(f,T)
    1.42          in (t,T) end
    1.43 -in List.concat o map (mk_cong_type sg o readfT) end;
    1.44 +in List.concat o map (mk_cong_type thy o readfT) end;
    1.45  
    1.46  end (* local *)
    1.47  end (* SIMP *);