1.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Wed Sep 07 14:51:58 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Wed Sep 07 15:01:17 2022 +0200
     1.3 @@ -46,33 +46,7 @@
     1.4    ML_file calculation.sml
     1.5  
     1.6  ML \<open>
     1.7 -\<close> text \<open>
     1.8 -fun lev_up [] = raise Ctree.PTREE "lev_up []"
     1.9 -  | lev_up p = (drop_last p);
    1.10 -\<close> text \<open>
    1.11 -lev_up: 'a list -> 'a list
    1.12 -\<close> text \<open>
    1.13 -lev_up: 'a list -> 'a list
    1.14 -\<close> text \<open>
    1.15 -open Ctree
    1.16 -\<close> text \<open> (*postpone after successful test*)
    1.17 -fun parent_node _ [] = (true, [], Rule_Set.Empty)
    1.18 -  | parent_node pt p =
    1.19 -    let
    1.20 -      fun par _ [] = (true, [], Rule_Set.Empty)
    1.21 -        | par pt p =
    1.22 -            if is_pblobj (get_obj I pt p)
    1.23 -            then (true, p, Rule_Set.Empty)
    1.24 -  		      else 
    1.25 -              let
    1.26 -                val ctxt = p |> get_obj g_loc pt |> snd |> the |> snd (*parent_node goes lev_up*)
    1.27 -              in
    1.28 -                case get_obj g_tac pt p of
    1.29 -      				    Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
    1.30 -      			    | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
    1.31 -      			    | _ => par pt (lev_up p)
    1.32 -              end
    1.33 -    in par pt (lev_up p) end; 
    1.34 +\<close> ML \<open>
    1.35  \<close> ML \<open>
    1.36  \<close>
    1.37  end