src/HOL/Tools/function_package/fundef_package.ML
changeset 19585 70a1ce3b23ae
parent 19583 c5fa77b03442
child 19611 da2a0014c461
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:21:13 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:22:05 2006 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4      in
     1.5  	thy |> ProofContext.init
     1.6  	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
     1.7 -	    (map (fn t => (("", []), [(t, ([], []))])) props)
     1.8 +	    (map (fn t => (("", []), [(t, [])])) props)
     1.9      end
    1.10  
    1.11  
    1.12 @@ -138,7 +138,7 @@
    1.13  	    |> ProofContext.note_thmss_i [(("termination_intro", 
    1.14  					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
    1.15  	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
    1.16 -	    [(("", []), [(goal, ([], []))])]
    1.17 +	    [(("", []), [(goal, [])])]
    1.18      end	
    1.19    | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
    1.20      let
    1.21 @@ -148,7 +148,7 @@
    1.22      in
    1.23  	thy |> ProofContext.init
    1.24  	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
    1.25 -	    [(("", []), [(subs, ([], [])), (dcl, ([], []))])]
    1.26 +	    [(("", []), [(subs, []), (dcl, [])])]
    1.27      end	
    1.28  
    1.29  
    1.30 @@ -192,4 +192,4 @@
    1.31  end;
    1.32  
    1.33  
    1.34 -end
    1.35 \ No newline at end of file
    1.36 +end