1.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Mon Apr 13 18:37:24 2020 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Tue Apr 14 12:39:26 2020 +0200
     1.3 @@ -41,13 +41,13 @@
     1.4  (*val it = 
     1.5    ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",
     1.6     "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)
     1.7 -map ThmC_Def.thmID_of_derivation_name' (thms_of thy) = 
     1.8 +map ThmC.thmID_of_derivation_name' (thms_of thy) = 
     1.9    ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", 
    1.10     "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]
    1.11  *)
    1.12  val thy = @{theory Biegelinie};
    1.13  val thms = thms_of thy;
    1.14 -if map ThmC_Def.thmID_of_derivation_name' thms = 
    1.15 +if map ThmC.thmID_of_derivation_name' thms = 
    1.16    ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", 
    1.17     "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
    1.18  else error "fun thms_of ...changed";
    1.19 @@ -144,10 +144,10 @@
    1.20  ;
    1.21  thydata2xml (theID, thydata);
    1.22  
    1.23 -"----------- fun Thm.make_thm ------------------------------------";
    1.24 -"----------- fun Thm.make_thm ------------------------------------";
    1.25 -"----------- fun Thm.make_thm ------------------------------------";
    1.26 -"~~~~~ fun Thm.make_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) =
    1.27 +"----------- fun ThmC_Def.make_thm ------------------------------------";
    1.28 +"----------- fun ThmC_Def.make_thm ------------------------------------";
    1.29 +"----------- fun ThmC_Def.make_thm ------------------------------------";
    1.30 +"~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : authors)) =
    1.31    (@{theory "Biegelinie"}, "IsacKnowledge",
    1.32      ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
    1.33  	      ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
    1.34 @@ -172,14 +172,14 @@
    1.35  "----------- fun revert_sym --------------------------------------";
    1.36  "----------- fun revert_sym --------------------------------------";
    1.37  val thy = @{theory Isac_Knowledge}
    1.38 -val (Thm (thmID, thm)) =
    1.39 -  revert_sym thy (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
    1.40 +val (Thm (thmID, thm)) = ThmC.revert_sym thy
    1.41 +  (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
    1.42  ;
    1.43  if thmID = "Poly.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z"
    1.44  then () else error "fun revert_sym changed 1";
    1.45  
    1.46 -val (Thm (thmID, thm)) =
    1.47 -  revert_sym thy (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
    1.48 +val (Thm (thmID, thm)) = ThmC.revert_sym thy
    1.49 +  (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
    1.50  ;
    1.51  if thmID = "Root.real_diff_minus" andalso string_of_thmI thm = "?a - ?b = ?a + -1 * ?b"
    1.52  then () else error "fun revert_sym changed 2"
    1.53 @@ -205,7 +205,7 @@
    1.54    |> flat
    1.55      (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
    1.56        Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
    1.57 -  |> map (revert_sym thy)
    1.58 +  |> map (ThmC.revert_sym thy)
    1.59      (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
    1.60        Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
    1.61    |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))