src/Pure/Isar/expression.ML
changeset 28832 cf7237498e7a
parent 28795 6891e273c33b
child 28852 5ddea758679b
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Nov 18 00:11:06 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Nov 18 09:40:06 2008 +0100
     1.3 @@ -499,83 +499,11 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* facts and attributes *)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -fun check_name name =
    1.12 -  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
    1.13 -  else name;
    1.14 -
    1.15 -fun prep_facts prep_name get intern ctxt elem = elem |> Element.map_ctxt
    1.16 -     {var = I, typ = I, term = I,
    1.17 -      name = Name.map_name prep_name,
    1.18 -      fact = get ctxt,
    1.19 -      attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
    1.20 -
    1.21 -in
    1.22 -
    1.23 -fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
    1.24 -fun cert_facts x = prep_facts I (K I) (K I) x;
    1.25 -
    1.26 -end;
    1.27 -
    1.28 -
    1.29 -(* activate elements in context, return elements and facts *)
    1.30 -
    1.31 -local
    1.32 -
    1.33 -fun axioms_export axs _ As =
    1.34 -  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
    1.35 -
    1.36 -
    1.37 -(* NB: derived ids contain only facts at this stage *)
    1.38 -
    1.39 -fun activate_elem (Fixes fixes) ctxt =
    1.40 -      ([], ctxt |> ProofContext.add_fixes_i fixes |> snd)
    1.41 -  | activate_elem (Constrains _) ctxt =
    1.42 -      ([], ctxt)
    1.43 -  | activate_elem (Assumes asms) ctxt =
    1.44 -      let
    1.45 -        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
    1.46 -        val ts = maps (map #1 o #2) asms';
    1.47 -        val (_, ctxt') =
    1.48 -          ctxt |> fold Variable.auto_fixes ts
    1.49 -          |> ProofContext.add_assms_i (axioms_export []) asms';
    1.50 -      in ([], ctxt') end
    1.51 -  | activate_elem (Defines defs) ctxt =
    1.52 -      let
    1.53 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    1.54 -        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    1.55 -            let val ((c, _), t') = LocalDefs.cert_def ctxt t
    1.56 -            in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
    1.57 -        val (_, ctxt') =
    1.58 -          ctxt |> fold (Variable.auto_fixes o #1) asms
    1.59 -          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
    1.60 -      in ([], ctxt') end
    1.61 -  | activate_elem (Notes (kind, facts)) ctxt =
    1.62 -      let
    1.63 -        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
    1.64 -        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
    1.65 -      in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end;
    1.66 -
    1.67 -in
    1.68 -
    1.69 -fun activate_elems prep_facts raw_elems ctxt =
    1.70 -  let
    1.71 -    val elems = map (prep_facts ctxt) raw_elems;
    1.72 -    val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt);
    1.73 -    val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
    1.74 -  in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end;
    1.75 -
    1.76 -end;
    1.77 -
    1.78 -
    1.79  (* full context statements: import + elements + conclusion *)
    1.80  
    1.81  local
    1.82  
    1.83 -fun prep_context_statement prep_expr prep_elems prep_facts
    1.84 +fun prep_context_statement prep_expr prep_elems
    1.85      do_close imprt elements raw_concl context =
    1.86    let
    1.87      val thy = ProofContext.theory_of context;
    1.88 @@ -590,7 +518,7 @@
    1.89            val ((parms, elems, concl), (spec, (_, _, defs))) = prep_elems do_close
    1.90              context elements raw_concl;
    1.91            val ((elems', _), ctxt') =
    1.92 -            activate_elems prep_facts elems (ProofContext.set_stmt true ctxt);
    1.93 +            Element.activate elems (ProofContext.set_stmt true ctxt);
    1.94          in
    1.95            (((ctxt', elems'), (parms, spec, defs)), concl)
    1.96          end
    1.97 @@ -607,10 +535,10 @@
    1.98  in
    1.99  
   1.100  fun read_context imprt body ctxt =
   1.101 -  #1 (prep_context_statement intern_expr read_elems read_facts true imprt body [] ctxt);
   1.102 +  #1 (prep_context_statement intern_expr read_elems true imprt body [] ctxt);
   1.103  (*
   1.104  fun cert_context imprt body ctxt =
   1.105 -  #1 (prep_context_statement (K I) cert_elems cert_facts true imprt body [] ctxt);
   1.106 +  #1 (prep_context_statement (K I) cert_elems true imprt body [] ctxt);
   1.107  *)
   1.108  end;
   1.109