src/Pure/thm.ML
changeset 2182 29e56f003599
parent 2177 8b365a3a6ed1
child 2193 b7e59795c75b
     1.1 --- a/src/Pure/thm.ML	Wed Nov 13 10:41:50 1996 +0100
     1.2 +++ b/src/Pure/thm.ML	Wed Nov 13 10:42:50 1996 +0100
     1.3 @@ -483,7 +483,8 @@
     1.4    in
     1.5      Thm {sign = sign, der = der, maxidx = maxidx,
     1.6  	 shyps =
     1.7 -	 (if eq_set (shyps',sorts) orelse not (!force_strip_shyps) then shyps'
     1.8 +	 (if eq_set_sort (shyps',sorts) orelse 
     1.9 +	     not (!force_strip_shyps) then shyps'
    1.10  	  else    (* FIXME tmp *)
    1.11  	      (writeln ("WARNING Removed sort hypotheses: " ^
    1.12  			commas (map Type.str_of_sort (shyps' \\ sorts)));
    1.13 @@ -503,7 +504,7 @@
    1.14    | xshyps =>
    1.15        let
    1.16          val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
    1.17 -        val shyps' = logicS ins (shyps \\ xshyps);
    1.18 +        val shyps' = ins_sort (logicS, shyps \\ xshyps);
    1.19          val used_names = foldr add_term_tfree_names (prop :: hyps, []);
    1.20          val names =
    1.21            tl (variantlist (replicate (length xshyps + 1) "'", used_names));
    1.22 @@ -1412,7 +1413,7 @@
    1.23    | vperm(t,u) = (t=u);
    1.24  
    1.25  fun var_perm(t,u) = vperm(t,u) andalso
    1.26 -                    eq_set(add_term_vars(t,[]), add_term_vars(u,[]))
    1.27 +                    eq_set_term (term_vars t, term_vars u)
    1.28  
    1.29  (*simple test for looping rewrite*)
    1.30  fun loops sign prems (lhs,rhs) =