1.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Sat Apr 17 21:37:31 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Sun Apr 18 13:01:05 2021 +0200
     1.3 @@ -96,19 +96,31 @@
     1.4    | _ =>
     1.5      thmid |> Global_Theory.get_thm thy |> numerals_to_Free
     1.6  
     1.7 +fun dest_eq_concl thm =
     1.8 +  (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of
     1.9 +    NONE => raise THM ("dest_eq_concl: conclusion needs to be HOL equality", 0, [thm])
    1.10 +  | SOME eq => eq);
    1.11 +
    1.12  (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
    1.13 +(*NB: careful instantiation avoids shifting of schematic variables*)
    1.14  fun sym_thm thm =
    1.15 -  let 
    1.16 -    val (derivation,
    1.17 -      {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps,
    1.18 -        hyps = hyps, tpairs = tpairs, prop = prop}) = Thm.rep_thm_G thm
    1.19 -    val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop
    1.20 -    val prop' = case TermC.strip_imp_prems' prop of
    1.21 -        NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))
    1.22 -      | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
    1.23 -  in
    1.24 -    Thm.assbl_thm derivation cert tags maxidx constraints shyps hyps tpairs prop'
    1.25 -  end
    1.26 +  let
    1.27 +    val thy = Thm.theory_of_thm thm;
    1.28 +    val certT = Thm.global_ctyp_of thy;
    1.29 +    val cert = Thm.global_cterm_of thy;
    1.30 +
    1.31 +    val (lhs, rhs) = dest_eq_concl thm |> apply2 cert;
    1.32 +    val A = Thm.typ_of_cterm lhs;
    1.33 +
    1.34 +    val sym_rule = Thm.lift_rule (Thm.cprop_of thm) @{thm sym};
    1.35 +    val (t, s) = dest_eq_concl sym_rule;
    1.36 +
    1.37 +    val instT = map (rpair A) (Term.add_tvars t []);
    1.38 +    val (t', s') = (t, s) |> apply2 (dest_Var o Term_Subst.instantiate (instT, []));
    1.39 +
    1.40 +    val cinstT = map (apsnd certT) instT;
    1.41 +    val cinst = [(s', lhs), (t', rhs)];
    1.42 +  in Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule) thm end;
    1.43  
    1.44  fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty
    1.45    | make_sym_rule_set (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =