1.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-present.sml	Sat Apr 17 20:44:57 2021 +0200
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-present.sml	Sat Apr 17 21:10:27 2021 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4  	     Applicable.Yes (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
     1.5  	       let
     1.6             val thm_deriv = Thm.get_name_hint thm
     1.7 -           val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
     1.8 +           val thminst = TermC.inst_bdv subst (Eval.norm (Thm.prop_of thm))
     1.9  	       in
    1.10  	         ContThmInst
    1.11  	          {thyID = thy',
    1.12 @@ -168,7 +168,7 @@
    1.13             val pp = Ctree.par_pblobj pt p
    1.14             val thy' = Ctree.get_obj Ctree.g_domID pt pp
    1.15             val subst = Subst.T_from_input (ThyC.get_theory thy') subs
    1.16 -           val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
    1.17 +           val thminst = TermC.inst_bdv subst (Eval.norm (Thm.prop_of thm))
    1.18             val f = case p_ of
    1.19                 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
    1.20               | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p