src/FOLP/simp.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 60644 4af8b9c2b52f
     1.1 --- a/src/FOLP/simp.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/FOLP/simp.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -436,7 +436,7 @@
     1.4        are represented by rules, generalized over their parameters*)
     1.5  fun add_asms(ss,thm,a,anet,ats,cs) =
     1.6      let val As = strip_varify(nth_subgoal i thm, a, []);
     1.7 -        val thms = map (Thm.trivial o Thm.cterm_of(Thm.theory_of_thm thm)) As;
     1.8 +        val thms = map (Thm.trivial o Thm.global_cterm_of(Thm.theory_of_thm thm)) As;
     1.9          val new_rws = maps mk_rew_rules thms;
    1.10          val rwrls = map mk_trans (maps mk_rew_rules thms);
    1.11          val anet' = fold_rev lhs_insert_thm rwrls anet;
    1.12 @@ -559,12 +559,12 @@
    1.13  fun mk_cong sg (f,aTs,rT) (refl,eq) =
    1.14  let val k = length aTs;
    1.15      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
    1.16 -        let val ca = Thm.cterm_of sg va
    1.17 -            and cx = Thm.cterm_of sg (eta_Var(("X"^si,0),T))
    1.18 -            val cb = Thm.cterm_of sg vb
    1.19 -            and cy = Thm.cterm_of sg (eta_Var(("Y"^si,0),T))
    1.20 -            val cP = Thm.cterm_of sg P
    1.21 -            and cp = Thm.cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
    1.22 +        let val ca = Thm.global_cterm_of sg va
    1.23 +            and cx = Thm.global_cterm_of sg (eta_Var(("X"^si,0),T))
    1.24 +            val cb = Thm.global_cterm_of sg vb
    1.25 +            and cy = Thm.global_cterm_of sg (eta_Var(("Y"^si,0),T))
    1.26 +            val cP = Thm.global_cterm_of sg P
    1.27 +            and cp = Thm.global_cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
    1.28          in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
    1.29      fun mk(c,T::Ts,i,yik) =
    1.30          let val si = radixstring(26,"a",i)