equal
deleted
inserted
replaced
449 fun is_exactly_equal (pt, pos as (p, _)) istr = |
449 fun is_exactly_equal (pt, pos as (p, _)) istr = |
450 case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> Rule.thy2ctxt) istr of |
450 case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> Rule.thy2ctxt) istr of |
451 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "") |
451 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "") |
452 | SOME ifo => |
452 | SOME ifo => |
453 let |
453 let |
454 val p' = Ctree.lev_on p; |
454 val p' = Pos.lev_on p; |
455 val tac = Ctree.get_obj Ctree.g_tac pt p'; |
455 val tac = Ctree.get_obj Ctree.g_tac pt p'; |
456 in |
456 in |
457 case Applicable.applicable_in pos pt tac of |
457 case Applicable.applicable_in pos pt tac of |
458 Applicable.Notappl msg => (msg, Tactic.Tac "") |
458 Applicable.Notappl msg => (msg, Tactic.Tac "") |
459 | Applicable.Appl rew => |
459 | Applicable.Appl rew => |