1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Apr 28 15:44:59 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Apr 28 16:51:36 2020 +0200
     1.3 @@ -106,6 +106,9 @@
     1.4  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     1.5    val typ_a2real: term -> term
     1.6  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
     1.7 +
     1.8 +(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
     1.9 +  val sym_trm : term -> term
    1.10  end
    1.11  
    1.12  (**)
    1.13 @@ -595,5 +598,14 @@
    1.14    |> member (fn (t1, t2) => fst (dest_Const t1) = fst (dest_Const t2)) ts
    1.15  ) handle TERM("dest_Const", _) => raise TERM ("contains_Const_typeless", [t])
    1.16  
    1.17 +(* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)
    1.18 +fun sym_trm trm =
    1.19 +  let
    1.20 +    val (lhs, rhs) = (dest_equals o strip_trueprop o Logic.strip_imp_concl) trm
    1.21 +    val trm' = case strip_imp_prems' trm of
    1.22 +	      NONE => mk_equality (rhs, lhs)
    1.23 +	    | SOME cs => ins_concl cs (mk_equality (rhs, lhs))
    1.24 +  in trm' end
    1.25 +
    1.26  
    1.27  end
    1.28 \ No newline at end of file