1.1 --- a/src/Pure/Isar/obtain.ML	Tue Sep 02 14:10:29 2008 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Sep 02 14:10:30 2008 +0200
     1.3 @@ -40,16 +40,16 @@
     1.4  signature OBTAIN =
     1.5  sig
     1.6    val thatN: string
     1.7 -  val obtain: string -> (string * string option * mixfix) list ->
     1.8 -    ((string * Attrib.src list) * (string * string list) list) list ->
     1.9 +  val obtain: string -> (Name.binding * string option * mixfix) list ->
    1.10 +    ((Name.binding * Attrib.src list) * (string * string list) list) list ->
    1.11      bool -> Proof.state -> Proof.state
    1.12 -  val obtain_i: string -> (string * typ option * mixfix) list ->
    1.13 -    ((string * attribute list) * (term * term list) list) list ->
    1.14 +  val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
    1.15 +    ((Name.binding * attribute list) * (term * term list) list) list ->
    1.16      bool -> Proof.state -> Proof.state
    1.17    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
    1.18      (cterm list * thm list) * Proof.context
    1.19 -  val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.20 -  val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.21 +  val guess: (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.22 +  val guess_i: (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.23  end;
    1.24  
    1.25  structure Obtain: OBTAIN =
    1.26 @@ -122,7 +122,7 @@
    1.27      (*obtain vars*)
    1.28      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
    1.29      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    1.30 -    val xs = map #1 vars;
    1.31 +    val xs = map (Name.name_of o #1) vars;
    1.32  
    1.33      (*obtain asms*)
    1.34      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    1.35 @@ -151,18 +151,19 @@
    1.36      fun after_qed _ =
    1.37        Proof.local_qed (NONE, false)
    1.38        #> Seq.map (`Proof.the_fact #-> (fn rule =>
    1.39 -        Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
    1.40 +        Proof.fix_i vars
    1.41          #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
    1.42    in
    1.43      state
    1.44      |> Proof.enter_forward
    1.45 -    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
    1.46 +    |> Proof.have_i NONE (K Seq.single) [((Name.no_binding, []), [(obtain_prop, [])])] int
    1.47      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    1.48 -    |> Proof.fix_i [(thesisN, NONE, NoSyn)]
    1.49 -    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
    1.50 +    |> Proof.fix_i [(Name.binding thesisN, NONE, NoSyn)]
    1.51 +    |> Proof.assume_i
    1.52 +      [((Name.binding that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
    1.53      |> `Proof.the_facts
    1.54      ||> Proof.chain_facts chain_facts
    1.55 -    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false
    1.56 +    ||> Proof.show_i NONE after_qed [((Name.no_binding, []), [(thesis, [])])] false
    1.57      |-> Proof.refine_insert
    1.58    end;
    1.59  
    1.60 @@ -258,8 +259,10 @@
    1.61      val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
    1.62    in ((vars', rule''), ctxt') end;
    1.63  
    1.64 -fun inferred_type (x, _, mx) ctxt =
    1.65 -  let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
    1.66 +fun inferred_type (binding, _, mx) ctxt =
    1.67 +  let
    1.68 +    val x = Name.name_of binding;
    1.69 +    val (T, ctxt') = ProofContext.inferred_param x ctxt
    1.70    in ((x, T, mx), ctxt') end;
    1.71  
    1.72  fun polymorphic ctxt vars =
    1.73 @@ -291,9 +294,9 @@
    1.74        in
    1.75          state'
    1.76          |> Proof.map_context (K ctxt')
    1.77 -        |> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms)
    1.78 -        |> `Proof.context_of |-> (fn fix_ctxt =>
    1.79 -            Proof.assm_i (obtain_export fix_ctxt rule (map cert ts)) [(("", []), asms)])
    1.80 +        |> Proof.fix_i (map (fn ((x, T), mx) => (Name.binding x, SOME T, mx)) parms)
    1.81 +        |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
    1.82 +          (obtain_export fix_ctxt rule (map cert ts)) [((Name.no_binding, []), asms)])
    1.83          |> Proof.add_binds_i AutoBind.no_facts
    1.84        end;
    1.85  
    1.86 @@ -308,10 +311,10 @@
    1.87      state
    1.88      |> Proof.enter_forward
    1.89      |> Proof.begin_block
    1.90 -    |> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)]
    1.91 +    |> Proof.fix_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)]
    1.92      |> Proof.chain_facts chain_facts
    1.93      |> Proof.local_goal print_result (K I) (apsnd (rpair I))
    1.94 -      "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]
    1.95 +      "guess" before_qed after_qed [((Name.no_binding, []), [Logic.mk_term goal, goal])]
    1.96      |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
    1.97    end;
    1.98