1.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Sat Jun 01 11:09:19 2019 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Sat Jun 22 13:15:52 2019 +0200
     1.3 @@ -26,7 +26,6 @@
     1.4      val get_calcs: theory -> term -> (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list
     1.5      val prep_rls: theory -> Rule.rls -> Rule.rls
     1.6      val prep_program : thm -> term
     1.7 -  val id_of_scr : term -> string
     1.8    val formal_args : term -> term list
     1.9    val body_of : term -> term
    1.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.11 @@ -53,7 +52,8 @@
    1.12    |> Thm.prop_of
    1.13    |> HOLogic.dest_Trueprop
    1.14    |> Logic.unvarify_global
    1.15 -  |> TermC.inst_abs)
    1.16 +  |> TermC.inst_abs
    1.17 +  |> TermC.numbers_to_string (*for numbers in the program*))
    1.18    handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])
    1.19  
    1.20  (* distinguish input to Model (deep embedding of terms as Isac's object language) *)
    1.21 @@ -101,7 +101,7 @@
    1.22    | get_fun_id t = raise TERM ("get_fun_id", [t])
    1.23  
    1.24  (* get the arguments of the script out of the scripts parsetree *)
    1.25 -fun formal_args tm = (tm (*TODO move to scrtools.sml*)
    1.26 +fun formal_args tm = (tm
    1.27    |> HOLogic.dest_eq
    1.28    |> fst
    1.29    |> strip_comb
    1.30 @@ -114,9 +114,6 @@
    1.31    |> snd)
    1.32    handle TERM _ => raise TERM ("body_of", [tm])
    1.33  
    1.34 -(* get the identifier of the script out of the scripts parsetree *)
    1.35 -fun id_of_scr sc = (id_of o fst o strip_comb) sc;
    1.36 -
    1.37  
    1.38  (** generate a "type calc" from a script **)
    1.39