1.1 --- a/src/Tools/isac/Interpret/mstools.sml	Wed May 29 14:22:31 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Thu May 30 12:04:55 2019 +0200
     1.3 @@ -33,8 +33,6 @@
     1.4  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
     1.5    val pblID_of_match : match -> Celem.pblID
     1.6    val refined_IDitms : match list -> match option
     1.7 -  val prep_program : thm -> term
     1.8 -(*val prep_program : theory -> string -> term *)
     1.9  end
    1.10  
    1.11  structure Stool(**) : SPECIFY_TOOL(**) =
    1.12 @@ -135,17 +133,6 @@
    1.13      val caller_ctxt = (scrval |> Model.dest_list' |> insert_assumptions) caller_ctxt
    1.14    in transfer_asms_from_to sub_ctxt caller_ctxt end;
    1.15  
    1.16 -(* prepare program for Lucas-Interpretation *)
    1.17 -(* version introduced BEFORE switch to partial_function *)
    1.18 -fun prep_program thy str = (TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) str
    1.19 -(* version for later switch to partial_function *)
    1.20 -fun prep_program thm = (thm
    1.21 -  |> Thm.prop_of
    1.22 -  |> HOLogic.dest_Trueprop
    1.23 -  |> Logic.unvarify_global
    1.24 -  |> TermC.inst_abs)
    1.25 -  handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])
    1.26 -
    1.27  fun common_subthy (thy1, thy2) =
    1.28    if Context.subthy (thy1, thy2) then thy2
    1.29    else if Context.subthy (thy2, thy1) then thy1