1.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml	Wed Feb 03 14:53:37 2021 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml	Wed Feb 03 15:21:12 2021 +0100
     1.3 @@ -14,7 +14,8 @@
     1.4    (theory -> Token.file list * theory) * 'c -> theory -> theory
     1.5    
     1.6    (* for keyword Problem*)
     1.7 -  val prove_vc: ParseC.problem -> Proof.context -> Proof.state
     1.8 +(**)val prove_vc: ParseC.problem -> Proof.context -> Proof.state(**)
     1.9 +(** )val prove_vc: ParseC.problem_headline -> Proof.context -> Proof.state( **)
    1.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.11  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.12  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.13 @@ -601,9 +602,7 @@
    1.14    if inthy = thy andalso inpbl = pbl
    1.15    then ((thy, pbl, met_id) : References.T, o_model)
    1.16    else ((inthy, inpbl, Method.id_empty), [])
    1.17 -(*
    1.18 -val prove_vc: ParseC.problem((_headline)) -> Proof.context -> Proof.state
    1.19 -*)
    1.20 +
    1.21  fun prove_vc (*vc_name*)problem lthy =
    1.22    let
    1.23      val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}