equal
deleted
inserted
replaced
26 then [get_obj g_tac pt p] |
26 then [get_obj g_tac pt p] |
27 else |
27 else |
28 let |
28 let |
29 val pp = par_pblobj pt p; |
29 val pp = par_pblobj pt p; |
30 val thy' = get_obj g_domID pt pp; |
30 val thy' = get_obj g_domID pt pp; |
31 val thy = Celem.assoc_thy thy'; |
31 val thy = ThyC.get_theory thy'; |
32 val metID = get_obj g_metID pt pp; |
32 val metID = get_obj g_metID pt pp; |
33 val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID |
33 val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID |
34 val (sc, srls) = (case Specify.get_met metID' of |
34 val (sc, srls) = (case Specify.get_met metID' of |
35 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1") |
35 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1") |
36 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst |
36 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst |
48 then [get_obj g_tac pt p] |
48 then [get_obj g_tac pt p] |
49 else |
49 else |
50 let |
50 let |
51 val pp = par_pblobj pt p |
51 val pp = par_pblobj pt p |
52 val thy' = get_obj g_domID pt pp |
52 val thy' = get_obj g_domID pt pp |
53 val thy = Celem.assoc_thy thy' |
53 val thy = ThyC.get_theory thy' |
54 val metID = get_obj g_metID pt pp |
54 val metID = get_obj g_metID pt pp |
55 val metID' = |
55 val metID' = |
56 if metID = Celem.e_metID |
56 if metID = Celem.e_metID |
57 then (thd3 o snd3) (get_obj g_origin pt pp) |
57 then (thd3 o snd3) (get_obj g_origin pt pp) |
58 else metID |
58 else metID |