1.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -16,9 +16,6 @@
     1.4  
     1.5  (* required in ProgLang BEFORE definition in ---------------vvv   *)
     1.6    val int_opt_of_string: string -> int option (* belongs to TermC *)
     1.7 -  val numerals_to_Free: thm -> thm            (* belongs to ThmC  *)
     1.8 -  val num_to_Free: term -> term               (* belongs to TermC *)
     1.9 -  val uminus_to_string: term -> term          (* belongs to TermC *)
    1.10  end
    1.11  
    1.12  (**)
    1.13 @@ -47,51 +44,4 @@
    1.14      case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE
    1.15    end;
    1.16  
    1.17 -
    1.18 -(** transform Isabelle's binary numerals to "Free (string, T)" **)
    1.19 -
    1.20 -val num_to_Free = (**)I(* Makarius 100308 *)
    1.21 -(** )
    1.22 -  let
    1.23 -    fun dest_num t =
    1.24 -      (case try HOLogic.dest_number t of
    1.25 -        SOME (T, i) => SOME (Free (signed_string_of_int i, T))
    1.26 -      | NONE => NONE);
    1.27 -    fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
    1.28 -      | to_str (t as (u1 $ u2)) =
    1.29 -          (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
    1.30 -      | to_str t = perhaps dest_num t;
    1.31 -  in to_str end
    1.32 -( **)
    1.33 -
    1.34 -val uminus_to_string = (**)I
    1.35 -(** )
    1.36 -  let
    1.37 -	  fun dest_num t =
    1.38 -	    case t of
    1.39 -	      (Const (\<^const_name>\<open>uminus\<close>, _) $ Free (s, T)) => 
    1.40 -	        (case int_opt_of_string s of
    1.41 -	          SOME i => SOME (Free (signed_string_of_int (~1 * i), T))
    1.42 -	        | NONE => NONE)
    1.43 -	    | _ => NONE;
    1.44 -    fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
    1.45 -      | to_str (t as (u1 $ u2)) =
    1.46 -          (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
    1.47 -      | to_str t = perhaps dest_num t;
    1.48 -  in to_str end;
    1.49 -( **)
    1.50 -
    1.51 -fun numerals_to_Free thm = (**)thm
    1.52 -(** )
    1.53 -  let
    1.54 -    val prop = Thm.plain_prop_of thm
    1.55 -    val prop' = num_to_Free prop;
    1.56 -  in
    1.57 -    if prop = prop' then thm
    1.58 -    else
    1.59 -      Skip_Proof.make_thm (Thm.theory_of_thm thm) prop'
    1.60 -      |> Thm.put_name_hint (Thm.get_name_hint thm)
    1.61 -  end;
    1.62 -( **)
    1.63 -
    1.64  (**)end(**)