src/Pure/Isar/proof.ML
changeset 9292 c5875175751f
parent 9196 1f6f66fe777a
child 9469 8058d285b1cd
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jul 13 11:38:42 2000 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jul 13 11:39:03 2000 +0200
     1.3 @@ -524,10 +524,13 @@
     1.4  (* invoke_case *)
     1.5  
     1.6  fun invoke_case (name, atts) state =
     1.7 -  let val (vars, props) = get_case state name in
     1.8 +  let
     1.9 +    val (vars, props) = get_case state name;
    1.10 +    val bind_skolem = ProofContext.bind_skolem (context_of state) (map #1 vars);
    1.11 +  in
    1.12      state
    1.13      |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
    1.14 -    |> assume_i [(name, atts, map (fn t => (t, ([], []))) props)]
    1.15 +    |> assume_i [(name, atts, map (fn t => (t, ([], []))) (map bind_skolem props))]
    1.16    end;
    1.17  
    1.18  
    1.19 @@ -565,7 +568,7 @@
    1.20    in
    1.21      state'
    1.22      |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
    1.23 -    |> map_context (ProofContext.add_cases (RuleCases.make goal [antN]))
    1.24 +    |> map_context (ProofContext.add_cases (RuleCases.make false goal [antN]))
    1.25      |> auto_bind_goal prop
    1.26      |> (if is_chain state then use_facts else reset_facts)
    1.27      |> new_block