equal
deleted
inserted
replaced
47 if Pos.on_specification pos |
47 if Pos.on_specification pos |
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 (*ctxt* ) |
52 val thy' = get_obj g_domID pt pp |
53 val thy' = get_obj g_domID pt pp |
53 val thy = ThyC.get_theory thy' |
54 val thy = ThyC.get_theory thy' |
|
55 ( **) |
|
56 val ctxt = Ctree.get_loc pt pos |> snd |
|
57 val thy = Proof_Context.theory_of ctxt |
|
58 (**) |
54 val metID = get_obj g_metID pt pp |
59 val metID = get_obj g_metID pt pp |
55 val metID' = |
60 val metID' = |
56 if metID = MethodC.id_empty |
61 if metID = MethodC.id_empty |
57 then (thd3 o snd3) (get_obj g_origin pt pp) |
62 then (thd3 o snd3) (get_obj g_origin pt pp) |
58 else metID |
63 else metID |