Args.context;
authorwenzelm
Thu Jun 26 15:06:25 2008 +0200 (2008-06-26)
changeset 273708e8f96dfaf63
parent 27369 7f242009f7b4
child 27371 f89aa7bd4602
Args.context;
src/HOL/Nominal/nominal_induct.ML
src/Pure/ML/ml_antiquote.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Jun 26 11:58:27 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Jun 26 15:06:25 2008 +0200
     1.3 @@ -134,8 +134,8 @@
     1.4        -- Args.term) >> SOME ||
     1.5      inst >> Option.map (pair NONE);
     1.6  
     1.7 -val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
     1.8 -  error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of ctxt) t));
     1.9 +val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
    1.10 +  error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
    1.11  
    1.12  fun unless_more_args scan = Scan.unless (Scan.lift
    1.13    ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
     2.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Jun 26 11:58:27 2008 +0200
     2.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Jun 26 15:06:25 2008 +0200
     2.3 @@ -58,9 +58,6 @@
     2.4  
     2.5  (** concrete antiquotations **)
     2.6  
     2.7 -fun context x = (Scan.state >> Context.proof_of) x;
     2.8 -
     2.9 -
    2.10  (* misc *)
    2.11  
    2.12  val _ = value "theory"
    2.13 @@ -74,7 +71,7 @@
    2.14  
    2.15  val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
    2.16  
    2.17 -val _ = inline "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) =>
    2.18 +val _ = inline "sort" (Args.context -- Scan.lift Args.name >> (fn (ctxt, s) =>
    2.19    ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
    2.20  
    2.21  val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
    2.22 @@ -91,11 +88,11 @@
    2.23    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
    2.24  
    2.25  val _ = value "cpat"
    2.26 -  (context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
    2.27 +  (Args.context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
    2.28      "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
    2.29  
    2.30  
    2.31 -fun type_ syn = (context -- Scan.lift Args.name >> (fn (ctxt, c) =>
    2.32 +fun type_ syn = (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
    2.33      #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
    2.34      |> syn ? Sign.base_name
    2.35      |> ML_Syntax.print_string));
    2.36 @@ -104,7 +101,7 @@
    2.37  val _ = inline "type_syntax" (type_ true);
    2.38  
    2.39  
    2.40 -fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) =>
    2.41 +fun const syn = Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
    2.42    #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
    2.43    |> syn ? ProofContext.const_syntax_name ctxt
    2.44    |> ML_Syntax.print_string);
    2.45 @@ -113,7 +110,7 @@
    2.46  val _ = inline "const_syntax" (const true);
    2.47  
    2.48  val _ = inline "const"
    2.49 -  (context -- Scan.lift Args.name --
    2.50 +  (Args.context -- Scan.lift Args.name --
    2.51      Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
    2.52      >> (fn ((ctxt, c), Ts) =>
    2.53        let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
     3.1 --- a/src/Tools/induct.ML	Thu Jun 26 11:58:27 2008 +0200
     3.2 +++ b/src/Tools/induct.ML	Thu Jun 26 15:06:25 2008 +0200
     3.3 @@ -718,8 +718,8 @@
     3.4        -- Args.term) >> SOME ||
     3.5      inst >> Option.map (pair NONE);
     3.6  
     3.7 -val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
     3.8 -  error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of context) t));
     3.9 +val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
    3.10 +  error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
    3.11  
    3.12  fun unless_more_args scan = Scan.unless (Scan.lift
    3.13    ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||