1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Fri Aug 08 17:08:10 2014 +0200
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Oct 23 16:40:58 2014 +0200
1.3 @@ -306,7 +306,7 @@
1.4 val isabthys' = map Context.theory_name (isabthys ());
1.5 in
1.6 if member op= isabthys' (thyID_of_derivation_name thmDeriv)
1.7 - then ("Isabelle", thmID_of_derivation_name thmDeriv)
1.8 + then ("Isabelle", thyID_of_derivation_name thmDeriv)
1.9 else ("IsacKnowledge", thyID_of_derivation_name thmDeriv)
1.10 end;
1.11
1.12 @@ -409,15 +409,14 @@
1.13 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) =
1.14 (case applicable_in pos pt tac of
1.15 Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>
1.16 - let
1.17 - val thmDeriv = "WN120320: AT Isa2009-2-->11 BROKEN"
1.18 - val thy = assoc_thy thy'
1.19 - val thm = (norm o #prop o rep_thm o (Global_Theory.get_thm thy)) thmID
1.20 + let
1.21 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
1.22 + val thm_deriv = Thm.get_name_hint thm
1.23 in
1.24 ContThm
1.25 {thyID = theory'2thyID thy',
1.26 thm =
1.27 - thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv),
1.28 + thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
1.29 applto = f,
1.30 applat = e_term,
1.31 reword = ord',
1.32 @@ -430,7 +429,8 @@
1.33 end
1.34 | Notappl _ =>
1.35 let
1.36 - val thmDeriv = "WN120320: AT Isa2009-2-->11 BROKEN"
1.37 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
1.38 + val thm_deriv = Thm.get_name_hint thm
1.39 val pp = par_pblobj pt p
1.40 val thy' = get_obj g_domID pt pp
1.41 val f = case p_ of
1.42 @@ -439,21 +439,22 @@
1.43 in
1.44 ContNOrew
1.45 {thyID = theory'2thyID thy',
1.46 - thm_rls = thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv),
1.47 + thm_rls =
1.48 + thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
1.49 applto = f}
1.50 - end)
1.51 -
1.52 + end)
1.53 | context_thy (pt, pos as (p,p_)) (tac as Rewrite_Inst (subs, (thmID,_))) =
1.54 (case applicable_in pos pt tac of
1.55 Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =>
1.56 let
1.57 - val thmDeriv = "WN120320: get this from a reference variable ?!?"
1.58 - val thm = (norm o #prop o rep_thm o (Global_Theory.get_thm (assoc_thy thy'))) thmID
1.59 - val thminst = inst_bdv subst thm
1.60 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
1.61 + val thm_deriv = Thm.get_name_hint thm
1.62 + val thminst = inst_bdv subst ((norm o #prop o rep_thm) thm)
1.63 in
1.64 ContThmInst
1.65 {thyID = theory'2thyID thy',
1.66 - thm = thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv),
1.67 + thm =
1.68 + thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
1.69 bdvs = subst,
1.70 thminst = thminst,
1.71 applto = f,
1.72 @@ -468,20 +469,19 @@
1.73 end
1.74 | Notappl _ =>
1.75 let
1.76 - val thmDeriv = "WN120320: get this from a reference variable ?!?"
1.77 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
1.78 + val thm_deriv = Thm.get_name_hint thm
1.79 val pp = par_pblobj pt p
1.80 val thy' = get_obj g_domID pt pp
1.81 val subst = subs2subst (assoc_thy thy') subs
1.82 - val thm = (norm o #prop o rep_thm o (Global_Theory.get_thm (assoc_thy thy'))) thmID
1.83 - val thminst = inst_bdv subst thm
1.84 + val thminst = inst_bdv subst ((norm o #prop o rep_thm) thm)
1.85 val f = case p_ of
1.86 Frm => get_obj g_form pt p
1.87 | Res => (fst o (get_obj g_result pt)) p
1.88 in
1.89 ContNOrewInst
1.90 {thyID = theory'2thyID thy',
1.91 - thm_rls =
1.92 - "WN120320: thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv)",
1.93 + thm_rls = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
1.94 bdvs = subst,
1.95 thminst = thminst,
1.96 applto = f}
1.97 @@ -491,7 +491,7 @@
1.98 Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) =>
1.99 ContRls
1.100 {thyID = theory'2thyID thy',
1.101 - rls = "WN120320: rls2guh (thy_containing_rls thy' rls') rls'",
1.102 + rls = rls2guh (thy_containing_rls thy' rls') rls',
1.103 applto = f,
1.104 result = res,
1.105 asms = asm})
1.106 @@ -500,7 +500,7 @@
1.107 Appl (Rewrite_Set_Inst' (thy', _, subst, rls, f, (res,asm))) =>
1.108 ContRlsInst
1.109 {thyID = theory'2thyID thy',
1.110 - rls = "WN120320: rls2guh (thy_containing_rls thy' rls') rls'",
1.111 + rls = rls2guh (thy_containing_rls thy' rls') rls',
1.112 bdvs = subst,
1.113 applto = f,
1.114 result = res,